多義語：theorem -- 定理

現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。

1. 辞書的意味
2. 証明が済んだ論理式（ほぼ、辞書的意味）
3. ML言語のthmデータ型
4. ML言語のthmデータ型のデータ（インスタンス）
5. Isarのtheoremコマンド
6. Isarのtheoremコマンドを使った宣言文
7. Isarのtheoremコマンドを使った宣言文の論理式部分
8. 証明が完了したときに生成されるシェマ変数（スキーム変数）を含んだシェマ論理式
9. コンテキストに格納されたシェマ論理式

ML言語のthmデータ型の影響が強い。ルール、ゴールなどもthmとして表現される。また、Isarのtheoremはlemma、propositionと書いても同じなので、この状況での定理と命題が同じになる。