equal
deleted
inserted
replaced
59 by (simp only: atomize_eq induct_equal_def) |
59 by (simp only: atomize_eq induct_equal_def) |
60 |
60 |
61 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" |
61 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" |
62 by (simp add: induct_implies_def) |
62 by (simp add: induct_implies_def) |
63 |
63 |
64 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq |
64 lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq |
65 lemmas induct_rulify1 = induct_atomize [symmetric, standard] |
65 lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq |
66 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def |
66 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def |
67 |
67 |
68 hide const induct_forall induct_implies induct_equal |
68 hide const induct_forall induct_implies induct_equal |
69 |
69 |
70 |
70 |