Added blast.ML as a dependency
authorpaulson
Fri Apr 04 11:17:05 1997 +0200 (1997-04-04)
changeset 2889a86f3b5f3cc7
parent 2888 e551e4bd262a
child 2890 f27002fc531d
Added blast.ML as a dependency
src/FOL/IsaMakefile
src/FOL/Makefile
src/HOL/IsaMakefile
src/HOL/Makefile
     1.1 --- a/src/FOL/IsaMakefile	Fri Apr 04 11:16:44 1997 +0200
     1.2 +++ b/src/FOL/IsaMakefile	Fri Apr 04 11:17:05 1997 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
     1.6  	thy_data.ML cladata.ML \
     1.7 -	../Provers/hypsubst.ML ../Provers/classical.ML \
     1.8 +	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
     1.9  	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    1.10  
    1.11  EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
     2.1 --- a/src/FOL/Makefile	Fri Apr 04 11:16:44 1997 +0200
     2.2 +++ b/src/FOL/Makefile	Fri Apr 04 11:17:05 1997 +0200
     2.3 @@ -21,10 +21,10 @@
     2.4  
     2.5  BIN = $(ISABELLEBIN)
     2.6  COMP = $(ISABELLECOMP)
     2.7 -FILES =	 ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
     2.8 -	 thy_data.ML cladata.ML \
     2.9 -	 ../Provers/hypsubst.ML ../Provers/classical.ML \
    2.10 -	 ../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    2.11 +FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    2.12 +	thy_data.ML cladata.ML \
    2.13 +	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
    2.14 +	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    2.15  
    2.16  EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
    2.17  EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML  ex/int.ML ex/intro.ML\
     3.1 --- a/src/HOL/IsaMakefile	Fri Apr 04 11:16:44 1997 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Fri Apr 04 11:17:05 1997 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
     3.5  	ind_syntax.ML cladata.ML simpdata.ML \
     3.6  	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
     3.7 -	../Provers/hypsubst.ML ../Provers/classical.ML \
     3.8 +	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
     3.9  	../Provers/simplifier.ML ../Provers/splitter.ML \
    3.10  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    3.11  
     4.1 --- a/src/HOL/Makefile	Fri Apr 04 11:16:44 1997 +0200
     4.2 +++ b/src/HOL/Makefile	Fri Apr 04 11:17:05 1997 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
     4.5  	ind_syntax.ML cladata.ML simpdata.ML\
     4.6  	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\
     4.7 -	../Provers/hypsubst.ML ../Provers/classical.ML\
     4.8 +	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
     4.9  	../Provers/simplifier.ML ../Provers/splitter.ML\
    4.10  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    4.11