src/HOL/Tools/inductive_package.ML
changeset 11831 d2421e124fa3
parent 11781 a08b62908caa
child 11834 02825c735938
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 18 21:03:43 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 18 21:05:35 2001 +0200
     1.3 @@ -73,10 +73,10 @@
     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 = "Inductive.forall";
     1.8 -val inductive_forall_def = thm "forall_def";
     1.9 -val inductive_conj_name = "Inductive.conj";
    1.10 -val inductive_conj_def = thm "conj_def";
    1.11 +val inductive_forall_name = "HOL.inductive_forall";
    1.12 +val inductive_forall_def = thm "inductive_forall_def";
    1.13 +val inductive_conj_name = "HOL.inductive_conj";
    1.14 +val inductive_conj_def = thm "inductive_conj_def";
    1.15  val inductive_conj = thms "inductive_conj";
    1.16  val inductive_atomize = thms "inductive_atomize";
    1.17  val inductive_rulify1 = thms "inductive_rulify1";