ひょっとして：証明コンスタント

proof constantって、登録されてた定理のことかも。

find_constsで定数を検索できる。その表示は、名前（ラベル）と型の組のリスト。find_theoremsでは、名前（ラベル）と命題（あるいはシーケント）の組のリスト。どちらも名前付けられているモノ。

モノが項（論理式含む）の構成に使われれときは、いわば項定数。モノが証明の構成に使われるなら、証明定数、ってことか？ 定義ないけど。

要するに、定数＝コンスタントというのは、「識別子の集合→モノ」という部分写像という解釈。Isabelleでは、「証明も項」と言えないので、項レベルの定数と証明レベルの定数、という区別がされる。そして、項レベルの定数を単にconsts、証明レベルの定数をfacts。証明レベルの定数は、定理にほかならないから、fact＝定理 なんだろう。

ただし、fact（単数）＝theorems（複数） という可能性はある。