--- 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)