src/FOL/FOL.thy
changeset 18511 beed2bc052a3
parent 18456 8cc35e95450a
child 18522 9bdfb6eaf8ab
equal deleted inserted replaced
18510:0a6c24f549c3 18511:beed2bc052a3
   110 lemma induct_conj_eq:
   110 lemma induct_conj_eq:
   111   includes meta_conjunction_syntax
   111   includes meta_conjunction_syntax
   112   shows "(A && B) == Trueprop(induct_conj(A, B))"
   112   shows "(A && B) == Trueprop(induct_conj(A, B))"
   113   by (unfold atomize_conj induct_conj_def)
   113   by (unfold atomize_conj induct_conj_def)
   114 
   114 
   115 lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
       
   116 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   115 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   117 lemmas induct_rulify [symmetric, standard] = induct_atomize
   116 lemmas induct_rulify [symmetric, standard] = induct_atomize
   118 lemmas induct_rulify_fallback =
   117 lemmas induct_rulify_fallback =
   119   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   118   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   120 
   119 
   125 
   124 
   126 ML {*
   125 ML {*
   127   structure InductMethod = InductMethodFun
   126   structure InductMethod = InductMethodFun
   128   (struct
   127   (struct
   129     val cases_default = thm "case_split";
   128     val cases_default = thm "case_split";
   130     val atomize_old = thms "induct_atomize_old";
       
   131     val atomize = thms "induct_atomize";
   129     val atomize = thms "induct_atomize";
   132     val rulify = thms "induct_rulify";
   130     val rulify = thms "induct_rulify";
   133     val rulify_fallback = thms "induct_rulify_fallback";
   131     val rulify_fallback = thms "induct_rulify_fallback";
   134   end);
   132   end);
   135 *}
   133 *}