# HG changeset patch
# User paulson
# Date 860145425 -7200
# Node ID a86f3b5f3cc781cdb11eb1eb12d9edc02f1b36ca
# Parent  e551e4bd262a87cb016c5591f7352b259dedb02c
Added blast.ML as a dependency

diff -r e551e4bd262a -r a86f3b5f3cc7 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Fri Apr 04 11:16:44 1997 +0200
+++ b/src/FOL/IsaMakefile	Fri Apr 04 11:17:05 1997 +0200
@@ -8,7 +8,7 @@
 
 FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
 	thy_data.ML cladata.ML \
-	../Provers/hypsubst.ML ../Provers/classical.ML \
+	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
 	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
 
 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
diff -r e551e4bd262a -r a86f3b5f3cc7 src/FOL/Makefile
--- a/src/FOL/Makefile	Fri Apr 04 11:16:44 1997 +0200
+++ b/src/FOL/Makefile	Fri Apr 04 11:17:05 1997 +0200
@@ -21,10 +21,10 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES =	 ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
-	 thy_data.ML cladata.ML \
-	 ../Provers/hypsubst.ML ../Provers/classical.ML \
-	 ../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
+FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
+	thy_data.ML cladata.ML \
+	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
+	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
 
 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML  ex/int.ML ex/intro.ML\
diff -r e551e4bd262a -r a86f3b5f3cc7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 04 11:16:44 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 04 11:17:05 1997 +0200
@@ -15,7 +15,7 @@
 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/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
 	../Provers/simplifier.ML ../Provers/splitter.ML \
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
diff -r e551e4bd262a -r a86f3b5f3cc7 src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Apr 04 11:16:44 1997 +0200
+++ b/src/HOL/Makefile	Fri Apr 04 11:17:05 1997 +0200
@@ -28,7 +28,7 @@
 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/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
 	../Provers/simplifier.ML ../Provers/splitter.ML\
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)