author | avigad |
Wed, 03 Aug 2005 14:48:22 +0200 | |
changeset 17010 | 5abc26872268 |
parent 17009 | 932e0e370926 |
child 17011 | 08f8408853e3 |
--- 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);