# HG changeset patch
# User paulson
# Date 912168802 -3600
# Node ID 2e9314c07146cffccd6b93815c9e8c83ce243b55
# Parent  11cbf236ca162df3242c49453a8599e114d2436b
added Real/Hyperreal

diff -r 11cbf236ca16 -r 2e9314c07146 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 27 11:24:27 1998 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 27 13:13:22 1998 +0100
@@ -135,7 +135,9 @@
   Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
   Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
   Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
-  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML
+  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
+  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
+  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy Real/Hyperreal/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Real