4.1 Proving tautologies

　命題論理の定理式（意味論での恒真式）のproverがTAUTであり，任意の定理式を証明してくれます．

TAUT`((p==>q)==>p)==>p`;;
val it : thm = |- ((p ==> q) ==> p) ==> p

　書き忘れていましたが，HOL Lightは普通の数学と同じく，古典論理を採用していますので，排中律が

TAUT `p \/ ˜p`;;
val it : thm = |- p \/ ˜p

のようにtheoremになります．