--- a/src/HOL/IsaMakefile Wed Jan 03 21:22:37 2001 +0100
+++ b/src/HOL/IsaMakefile Wed Jan 03 21:23:13 2001 +0100
@@ -70,9 +70,9 @@
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/make_elim.ML \
$(SRC)/Provers/rulify.ML $(SRC)/Provers/simplifier.ML \
$(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
- $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sml \
- $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml Calculation.thy \
+ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
+ $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
+ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
@@ -120,6 +120,7 @@
Real/RealPow.thy Real/real_arith.ML
@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
+
## HOL-Hyperreal
HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal