| This article or section describes an undocumented feature of Twelf.|
The information may be incomplete and subject to change.
keyword, when it precedes another directive such as a %total
directive, causes Twelf to believe that the directive succeeded even if it did not. This feature is only available in unsafe mode
, and can be used to easily create holes in metatheorems