# HG changeset patch
# User wenzelm
# Date 978553393 -3600
# Node ID 115c65650be3aee6d21fab18a3d5a38116cf6219
# Parent  662727d4ecac13fdb211fa6380befd255903cd4c
TFL: renamed .sml to .ML;

diff -r 662727d4ecac -r 115c65650be3 src/HOL/IsaMakefile
--- 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