Thms
bool
1
Doc
btrue
Def
true
==
Thm* true