--- a/TFL/thms.sig Tue May 20 11:47:33 1997 +0200
+++ b/TFL/thms.sig Tue May 20 11:49:57 1997 +0200
@@ -1,16 +1,15 @@
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 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 COND_CONG :thm
+ val LET_CONG :thm
- val eqT :Thm
- val rev_eq_mp :Thm
- val simp_thm :Thm
+ val eqT :thm
+ val rev_eq_mp :thm
+ val simp_thm :thm
end;