# HG changeset patch
# User wenzelm
# Date 999296406 -7200
# Node ID 97305ee424a9495944d6af623869b8f8d033f605
# Parent  d61b913431c55d93649b3ab8644ca48f5bcdd216
HOL-Real-Hyperreal made a plain session (no longer an image);

diff -r d61b913431c5 -r 97305ee424a9 src/HOL/Hyperreal/README.html
--- a/src/HOL/Hyperreal/README.html	Sat Sep 01 00:14:16 2001 +0200
+++ b/src/HOL/Hyperreal/README.html	Sat Sep 01 00:20:06 2001 +0200
@@ -8,7 +8,7 @@
 
 <UL>
 <LI><A HREF="Zorn.html">Zorn</A>
-Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
+Zorn's Lemma: proof based on the ZF version.
 
 <LI><A HREF="Filter.html">Filter</A>
 Theory of Filters and Ultrafilters.
@@ -55,5 +55,3 @@
 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
 </ADDRESS>
 </BODY></HTML>
-
-
diff -r d61b913431c5 -r 97305ee424a9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Sep 01 00:14:16 2001 +0200
+++ b/src/HOL/IsaMakefile	Sat Sep 01 00:20:06 2001 +0200
@@ -7,7 +7,7 @@
 ## targets
 
 default: HOL
-images: HOL HOL-Real HOL-Hyperreal TLA
+images: HOL HOL-Real TLA
 
 #Note: keep targets sorted (except for HOL-Library)
 test: \
@@ -17,6 +17,7 @@
   HOL-AxClasses \
   HOL-CTL \
       HOL-Real-HahnBanach \
+      HOL-Real-Hyperreal \
       HOL-Real-ex \
   HOL-GroupTheory \
   HOL-Hoare \
@@ -127,29 +128,26 @@
 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
 
-## HOL-Hyperreal
+## HOL-Real-Hyperreal
 
-HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal
+HOL-Real-Hyperreal: HOL-Real $(LOG)/HOL-Real-Hyperreal.gz
 
-$(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML \
-  Hyperreal/Filter.ML Hyperreal/Filter.thy \
-  Hyperreal/HRealAbs.ML Hyperreal/HRealAbs.thy \
-  Hyperreal/HSeries.ML Hyperreal/HSeries.thy \
-  Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy \
-  Hyperreal/hypreal_arith0.ML Hyperreal/hypreal_arith.ML \
-  Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
-  Hyperreal/HyperDef.ML Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML \
-  Hyperreal/HyperNat.thy Hyperreal/HyperOrd.ML \
-  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML \
-  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy \
-  Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/NSA.ML \
-  Hyperreal/NSA.thy Hyperreal/NatStar.ML \
-  Hyperreal/NatStar.thy Hyperreal/SEQ.ML \
-  Hyperreal/SEQ.thy Hyperreal/Series.ML \
-  Hyperreal/Series.thy Hyperreal/Star.ML \
-  Hyperreal/Star.thy Hyperreal/Zorn.ML \
-  Hyperreal/Zorn.thy Hyperreal/fuf.ML
-	@cd Hyperreal; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal
+$(LOG)/HOL-Real-Hyperreal.gz: $(OUT)/HOL-Real \
+  Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML \
+  Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy \
+  Hyperreal/HyperArith.thy Hyperreal/HyperArith0.ML \
+  Hyperreal/HyperArith0.thy Hyperreal/HyperBin.ML \
+  Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML Hyperreal/HyperDef.thy \
+  Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy Hyperreal/HyperOrd.ML \
+  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML Hyperreal/HyperPow.thy \
+  Hyperreal/Hyperreal.thy Hyperreal/Lim.ML Hyperreal/Lim.thy \
+  Hyperreal/NSA.ML Hyperreal/NSA.thy Hyperreal/NatStar.ML \
+  Hyperreal/NatStar.thy Hyperreal/ROOT.ML Hyperreal/SEQ.ML \
+  Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy \
+  Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Zorn.ML \
+  Hyperreal/Zorn.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
+  Hyperreal/hypreal_arith0.ML
+	@$(ISATOOL) usedir $(OUT)/HOL-Real Hyperreal
 
 
 ## HOL-Real-ex
@@ -613,6 +611,7 @@
 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
+		$(LOG)/HOL-Real-Hyperreal.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
 		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
 		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz