Prints as !

Use a theorem as a lemma in the current proof.

If the line already exists, ETPS will check whether it is a legal

instance of the theorem schema, otherwise it will prompt for the

metavariables in the theorem schema (usually x or P, Q, ...).

The command format for ASSERT is:

<n>ASSERT THEOREM LINE

"THEOREM" "LINE"

The arguments have the following meaning:

THEOREM : Name of Theorem

LINE : Line with Theorem Instance

Prints as !

Prints as !

© 1988-99, Carnegie Mellon University.