Added blast.ML as a dependency
authorpaulson
Fri, 04 Apr 1997 11:17:05 +0200
changeset 2889 a86f3b5f3cc7
parent 2888 e551e4bd262a
child 2890 f27002fc531d
Added blast.ML as a dependency
src/FOL/IsaMakefile
src/FOL/Makefile
src/HOL/IsaMakefile
src/HOL/Makefile
--- 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
--- 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\
--- 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)
 
--- 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)