TFL/thms.sml
changeset 6498 1ebbe18fe236
parent 3458 5ff4bfab859c
child 9867 bf8300fa4238
equal deleted inserted replaced
6497:120ca2bb27e1 6498:1ebbe18fe236
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 structure Thms : Thms_sig =
     7 structure Thms : Thms_sig =
     8 struct
     8 struct
     9    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
     9    val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
    10    val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
    10    val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
    11    val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
       
    12    val CUT_DEF = cut_def
    11    val CUT_DEF = cut_def
    13 
    12 
    14    local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
    13    local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
    15          val _ = by (strip_tac 1)
    14          val _ = by (strip_tac 1)
    16          val _ = by (rtac selectI 1)
    15          val _ = by (rtac selectI 1)