changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
authoravigad
Wed, 03 Aug 2005 14:48:22 +0200
changeset 17010 5abc26872268
parent 17009 932e0e370926
child 17011 08f8408853e3
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Aug 03 14:48:13 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 03 14:48:22 2005 +0200
@@ -65,8 +65,8 @@
 (** theory context references **)
 
 val mono_name = "Orderings.mono";
-val gfp_name = "Gfp.gfp";
-val lfp_name = "Lfp.lfp";
+val gfp_name = "FixedPoint.gfp";
+val lfp_name = "FixedPoint.lfp";
 val vimage_name = "Set.vimage";
 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);