## THM

prove a theorem
Major Section: OTHER

Example:
(thm (equal (app (app a b) c)
(app a (app b c))))

Also see defthm. Unlike `defthm`

, `thm`

does not create an
event; it merely causes the theorem prover to attempt a proof.

General Form:
(thm term
:hints hints
:otf-flg otf-flg
:doc doc-string)

where `term`

is a term alleged to be a theorem, and `hints`

,
`otf-flg`

and `doc-string`

are as described in the corresponding
`:`

`doc`

entries. The three keyword arguments above are all
optional.