Set.vimage;
authorwenzelm
Wed Nov 21 00:34:06 2001 +0100 (2001-11-21 ago)
changeset 122593949e7aba298
parent 12258 5da24e7e9aba
child 12260 4898247d0102
Set.vimage;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Nov 21 00:33:40 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 21 00:34:06 2001 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  val mono_name = "HOL.mono";
     1.5  val gfp_name = "Gfp.gfp";
     1.6  val lfp_name = "Lfp.lfp";
     1.7 -val vimage_name = "Inverse_Image.vimage";
     1.8 +val vimage_name = "Set.vimage";
     1.9  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    1.10  
    1.11  val inductive_forall_name = "HOL.induct_forall";