src/HOL/Tools/inductive_package.ML
changeset 11991 da6ee05d9f3d
parent 11880 a625de9ad62a
child 12109 bd6eb9194a5d
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Oct 31 01:21:01 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Oct 31 01:21:31 2001 +0100
     1.3 @@ -72,14 +72,14 @@
     1.4  val vimage_name = "Inverse_Image.vimage";
     1.5  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
     1.6  
     1.7 -val inductive_forall_name = "HOL.inductive_forall";
     1.8 -val inductive_forall_def = thm "inductive_forall_def";
     1.9 -val inductive_conj_name = "HOL.inductive_conj";
    1.10 -val inductive_conj_def = thm "inductive_conj_def";
    1.11 -val inductive_conj = thms "inductive_conj";
    1.12 -val inductive_atomize = thms "inductive_atomize";
    1.13 -val inductive_rulify1 = thms "inductive_rulify1";
    1.14 -val inductive_rulify2 = thms "inductive_rulify2";
    1.15 +val inductive_forall_name = "HOL.induct_forall";
    1.16 +val inductive_forall_def = thm "induct_forall_def";
    1.17 +val inductive_conj_name = "HOL.induct_conj";
    1.18 +val inductive_conj_def = thm "induct_conj_def";
    1.19 +val inductive_conj = thms "induct_conj";
    1.20 +val inductive_atomize = thms "induct_atomize";
    1.21 +val inductive_rulify1 = thms "induct_rulify1";
    1.22 +val inductive_rulify2 = thms "induct_rulify2";
    1.23  
    1.24  
    1.25