# %establish

From The Twelf Project

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.