# Thm

Prove a theorem

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

Also see defthm. Unlike `defthm`, thm does not store an
event; it merely causes the theorem prover to attempt a proof. But like
defthm, calls of thm are legal in event contexts (see embedded-event-form).

General Form:
(thm term
:instructions instructions
:hints hints
:otf-flg otf-flg)

where term is a term alleged to be a theorem, and `instructions`, `hints`, and `otf-flg` are as described in the
corresponding documentation topics. The keyword arguments are
optional.

For information on how thm is implemented using `make-event`,
see make-event-example-3.

### Subtopics

- Otf-flg
- Allow more than one initial subgoal to be pushed for induction
- Rule
- A thm-like version of defrule.