prove a theorem
Major Section:  OTHER

(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.