src/HOL/Inductive.thy

   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
   Collect_mono in_mono vimage_mono
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
   Ball_def Bex_def
-  inductive_rulify2
+  induct_rulify2
 
 
 subsubsection {* Inductive datatypes and primitive recursion *}
 
 text {* Package setup. *}