equal
deleted
inserted
replaced
53 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
53 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
54 notE' impE' impE iffE imp_cong simp_thms eq_True eq_False |
54 notE' impE' impE iffE imp_cong simp_thms eq_True eq_False |
55 induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
55 induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
56 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
56 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
57 induct_atomize induct_rulify induct_rulify_fallback |
57 induct_atomize induct_rulify induct_rulify_fallback |
58 True_implies_equals |
58 True_implies_equals TrueE |
59 |
59 |
60 datatype sumbool = Left | Right |
60 datatype sumbool = Left | Right |
61 |
61 |
62 subsection {* Type of extracted program *} |
62 subsection {* Type of extracted program *} |
63 |
63 |