ASSERT : CONCEPT-CHAR

ASSERT is a concept special character.
Prints as !

TPS documentation homepage


ASSERT : MEXPR

ASSERT is a top-level command.
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

TPS documentation homepage


ASSERT : SCRIBE-CHAR

ASSERT is a scribe special character.
Prints as !

TPS documentation homepage


ASSERT : TEX-CHAR

ASSERT is a tex special character.
Prints as !

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage