src/HOL/Tools/TFL/thms.ML
changeset 58184 db1381d811ab
parent 39159 0dec18004e75
     1.1 --- a/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  struct
     1.5    val WFREC_COROLLARY = @{thm tfl_wfrec};
     1.6    val WF_INDUCTION_THM = @{thm tfl_wf_induct};
     1.7 -  val CUT_DEF = @{thm cut_def};
     1.8 +  val CUT_DEF = @{thm tfl_cut_def};
     1.9    val eqT = @{thm tfl_eq_True};
    1.10    val rev_eq_mp = @{thm tfl_rev_eq_mp};
    1.11    val simp_thm = @{thm tfl_simp_thm};