equal
deleted
inserted
replaced
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"; |