src/HOL/IsaMakefile

   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(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 \
   Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
   Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \

   Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
   Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \
   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
 
 $(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML \