TFL/thms.sig

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thms.sig	Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,16 @@
+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;