From The Twelf Project
Jump to: navigation, search

The %prove directive attempts to prove a theorem specified by a %theorem directive using the theorem prover. It is therefore similar to the %establish directive. However, unlike the %establish directive, theorems shown to be true by the %prove directive are considered as potential lemmas when the theorem prover attempts to prove future theorems.

See also