# HG changeset patch
# User avigad
# Date 1123073310 -7200
# Node ID 08f8408853e34728db0f463279052bbfbdb1eabd
# Parent  5abc26872268bb859c8f2b7b05a5e5dfd996cd8b
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint

diff -r 5abc26872268 -r 08f8408853e3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 03 14:48:22 2005 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 03 14:48:30 2005 +0200
@@ -80,13 +80,13 @@
   $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
   Binomial.thy Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \
   Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
-  Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
+  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
   Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy		\
   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
   Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
   Integ/cooper_proof.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
   Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
-  Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy		\
+  Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy		\
   Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
   Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
@@ -150,7 +150,7 @@
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy					\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy				\
   Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy			\
-  Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy					\
+  Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy		\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
   Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
   Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\