- ユーザー定義の定理〈名前付き証明〉の名前には、赤で下線。
- システム組み込みの定理〈証明規則〉の名前には、青で下線。
- キーワード generic は総称〈多相〉の定理
- ユーザー定義の定理〈名前付き証明〉の呼び出しは、ピンクで下線。
- システム組み込みの定理〈証明規則〉の呼び出しは、水色で下線。
- 暗黙の仮定〈予備知識〉にあると想定する法則の結論のラベルは紫枠。
- テンプレートは箱で、テンプレート名は大文字。
- ドットからの命題は、暗黙の仮定〈予備知識〉にある法則の結論を取り出す。
- 分岐するドットはコピー。
- 黒三角は、仮定が空な証明規則〈システム組み込み〉
- レンガ色と薄緑色はコメント／ヒント
