changeset 3245 | 241838c01caf |
parent 3191 | 14bd6e5985f1 |
child 3273 | 114704740c86 |
--- a/TFL/thms.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/thms.sml Tue May 20 11:49:57 1997 +0200 @@ -1,7 +1,5 @@ structure Thms : Thms_sig = struct - type Thm = Thm.thm - val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec" val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct" val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"