TFL/thms.sml
changeset 3245 241838c01caf
parent 3191 14bd6e5985f1
child 3273 114704740c86
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     1 structure Thms : Thms_sig =
     1 structure Thms : Thms_sig =
     2 struct
     2 struct
     3    type Thm = Thm.thm
       
     4 
       
     5    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
     3    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
     6    val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
     4    val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
     7    val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
     5    val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
     8    val CUT_DEF = cut_def
     6    val CUT_DEF = cut_def
     9 
     7