--- 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 \