%establish

The %establish directive attempts to prove a theorem specified by a %theorem directive using the theorem prover. It is therefore similar to the %prove directive. However, unlike the %prove directive, theorems shown to be true by the %establish directive are not used to prove other theorems.

See also

• Theorem prover
• Theorem Prover (guide §10.57)