TFL/thms.ML
changeset 11455 e07927b980ec
parent 10769 70b9b0cfe05f
equal deleted inserted replaced
11454:7514e5e21cb8 11455:e07927b980ec
     7 structure Thms =
     7 structure Thms =
     8 struct
     8 struct
     9   val WFREC_COROLLARY = thm "tfl_wfrec";
     9   val WFREC_COROLLARY = thm "tfl_wfrec";
    10   val WF_INDUCTION_THM = thm "tfl_wf_induct";
    10   val WF_INDUCTION_THM = thm "tfl_wf_induct";
    11   val CUT_DEF = thm "cut_def";
    11   val CUT_DEF = thm "cut_def";
    12   val SELECT_AX = thm "tfl_some";
       
    13   val eqT = thm "tfl_eq_True";
    12   val eqT = thm "tfl_eq_True";
    14   val rev_eq_mp = thm "tfl_rev_eq_mp";
    13   val rev_eq_mp = thm "tfl_rev_eq_mp";
    15   val simp_thm = thm "tfl_simp_thm";
    14   val simp_thm = thm "tfl_simp_thm";
    16   val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
    15   val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
    17   val imp_trans = thm "tfl_imp_trans";
    16   val imp_trans = thm "tfl_imp_trans";