前回お話したtoplevel loopにおいてできることの２つ目は，evaluate expressions，つまり，数や文字列の評価でした． 「HOL Lightは，これに加えて，数学的陳述や論理的主張を表す「term」と，証明済みの主張を表す「theorem」を評価するツールの集まりです…

今回からしばらく 『HOL Light Tutorial (for version 2.20)』 http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf に従って話を進めます．なお，リファレンスはこちら 『The HOL Light System REFERENCE』 (For HOL Light 2.20++ November 2, 2011…