changeset 6498 | 1ebbe18fe236 |
parent 3458 | 5ff4bfab859c |
child 9867 | bf8300fa4238 |
--- a/TFL/thms.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/thms.sml Fri Apr 23 12:23:21 1999 +0200 @@ -6,9 +6,8 @@ structure Thms : Thms_sig = struct - 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" + val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec" + val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct" val CUT_DEF = cut_def local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"