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.
