# HG changeset patch
# User paulson
# Date 864120825 -7200
# Node ID 19a2b853ba7bcbe97856c03e71e77213709f6ed6
# Parent  6d1768e1d9bc67d4a2f02d241bd2d854c09563ce
Removal of ex/LexProd;  TFL files;  new treatment of Prover files

diff -r 6d1768e1d9bc -r 19a2b853ba7b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 20 11:33:02 1997 +0200
+++ b/src/HOL/IsaMakefile	Tue May 20 11:33:45 1997 +0200
@@ -12,13 +12,18 @@
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
 	Sexp Univ List RelPow Option
 
+PROVERS = hypsubst.ML classical.ML blast.ML \
+	simplifier.ML splitter.ML nat_transitive.ML 
+
+TFL   = dcterm.sml mask.sig mask.sml post.sml rules.new.sml rules.sig \
+	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
+	usyntax.sig usyntax.sml utils.sig utils.sml
+
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
 	ind_syntax.ML cladata.ML simpdata.ML \
 	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
-	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
-	../Provers/simplifier.ML ../Provers/splitter.ML \
-	../Provers/nat_transitive.ML \
-	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
+	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
+	$(PROVERS:%=../Provers/%)
 
 $(OUT)/HOL: $(OUT)/Pure $(FILES)
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
@@ -195,7 +200,7 @@
 
 ## Miscellaneous examples
 
-EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
+EX_NAMES = String BT InSort Qsort Puzzle Primes NatSum MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)