# HG changeset patch
# User paulson
# Date 978346280 -3600
# Node ID 8cd507be713898e3fde42f6b04840b61c175da80
# Parent  831c864cc56e53dee099903a92196f7d154b290f
put in some missing Hyperreal files

diff -r 831c864cc56e -r 8cd507be7138 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jan 01 11:50:31 2001 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 01 11:51:20 2001 +0100
@@ -94,8 +94,8 @@
   Tools/datatype_package.ML Tools/datatype_prop.ML \
   Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
   Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
-  Tools/primrec_package.ML Tools/recdef_package.ML Tools/record_package.ML \
-  Tools/string_syntax.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+  Tools/primrec_package.ML Tools/recdef_package.ML \
+  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
   Transitive_Closure.ML Transitive_Closure.thy Wellfounded_Recursion.ML \
   Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
@@ -124,9 +124,10 @@
 
 HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal
 
-$(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real \
+$(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 \