equal
deleted
inserted
replaced
29 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
29 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
30 notE' impE' impE iffE imp_cong simp_thms eq_True eq_False |
30 notE' impE' impE iffE imp_cong simp_thms eq_True eq_False |
31 induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
31 induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
32 induct_atomize induct_atomize' induct_rulify induct_rulify' |
32 induct_atomize induct_atomize' induct_rulify induct_rulify' |
33 induct_rulify_fallback induct_trueI |
33 induct_rulify_fallback induct_trueI |
34 True_implies_equals TrueE |
34 True_implies_equals implies_True_equals TrueE |
|
35 False_implies_equals |
35 |
36 |
36 lemmas [extraction_expand_def] = |
37 lemmas [extraction_expand_def] = |
37 HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def |
38 HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def |
38 HOL.induct_true_def HOL.induct_false_def |
39 HOL.induct_true_def HOL.induct_false_def |
39 |
40 |