The %theorem declaration acts as the specification of a theorem.
Use to write statements of metatheorems
Some people find the notation a clearer way of specifying metatheorems; a %theorem declaration used in this style handles the type family declation and the %mode declaration parts of a totality assertion.
Use with the theorem prover
When using the Twelf theorem prover, a %theorem declaration establishes a proposition that the theorem prover may later attempt to establish. A %theorem declaration is thus somewhat analogous to the three-part specification of a totality assertions, the type family definition, the %mode declaration, and the %worlds declaration.