From The Twelf Project
Jump to: navigation, search

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