Major Section: OTHER
Example: (thm (equal (app (app a b) c) (app a (app b c))))Also see defthm. Unlike
thmdoes 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
termis a term alleged to be a theorem, and
doc-stringare as described in the corresponding
docentries. The three keyword arguments above are all optional.