theorem f: P ≝ p

Proves a new theorem f whose thesis is P.

If p is provided, it must be a proof term for P. Otherwise an interactive proof is started.

P can be omitted only if the proof is not interactive.

A warning is raised if the name of the theorem cannot be obtained by mangling the name of the constants in its thesis.

Notice that the command is equivalent to definition f: T ≝ t.

corollary f: T ≝ t

Same as theorem f: T ≝ t

lemma f: T ≝ t

Same as theorem f: T ≝ t

fact f: T ≝ t

Same as theorem f: T ≝ t

example f: T ≝ t

Same as theorem f: T ≝ t, but the example is not indexed nor used by automation.