TFL/thms.sig

+signature Thms_sig =
+sig
+   type Thm
+   val WF_INDUCTION_THM:Thm
+   val WFREC_COROLLARY :Thm
+   val CUT_DEF         :Thm
+   val CUT_LEMMA       :Thm
+   val SELECT_AX       :Thm
+   
+   val COND_CONG :Thm
+   val LET_CONG  :Thm
+
+   val eqT       :Thm
+   val rev_eq_mp :Thm
+   val simp_thm  :Thm
+end;