new file Provers/make_elim.ML
authorpaulson
Wed Jun 28 10:37:08 2000 +0200 (2000-06-28)
changeset 9157998dd2fb5795
parent 9156 b9fe44ad3381
child 9158 084abf3d0eff
new file Provers/make_elim.ML
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/FOL/IsaMakefile	Tue Jun 27 23:43:46 2000 +0200
     1.2 +++ b/src/FOL/IsaMakefile	Wed Jun 28 10:37:08 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  Pure:
     1.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.6  
     1.7 -$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	\
     1.8 +$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
     1.9    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.10    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \
    1.11    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \
     2.1 --- a/src/FOL/ROOT.ML	Tue Jun 27 23:43:46 2000 +0200
     2.2 +++ b/src/FOL/ROOT.ML	Wed Jun 28 10:37:08 2000 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4  use "~~/src/Provers/splitter.ML";
     2.5  use "~~/src/Provers/ind.ML";
     2.6  use "~~/src/Provers/hypsubst.ML";
     2.7 +use "~~/src/Provers/make_elim.ML";
     2.8  use "~~/src/Provers/classical.ML";
     2.9  use "~~/src/Provers/blast.ML";
    2.10  use "~~/src/Provers/clasimp.ML";
     3.1 --- a/src/HOL/IsaMakefile	Tue Jun 27 23:43:46 2000 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Jun 28 10:37:08 2000 +0200
     3.3 @@ -36,7 +36,8 @@
     3.4    $(SRC)/Provers/Arith/assoc_fold.ML		\
     3.5    $(SRC)/Provers/Arith/combine_numerals.ML	\
     3.6    $(SRC)/Provers/Arith/cancel_numerals.ML	\
     3.7 -  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
     3.8 +  $(SRC)/Provers/Arith/fast_lin_arith.ML \
     3.9 +  $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
    3.10    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    3.11    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    3.12    $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
     4.1 --- a/src/HOL/ROOT.ML	Tue Jun 27 23:43:46 2000 +0200
     4.2 +++ b/src/HOL/ROOT.ML	Wed Jun 28 10:37:08 2000 +0200
     4.3 @@ -20,6 +20,7 @@
     4.4  use "~~/src/Provers/split_paired_all.ML";
     4.5  use "~~/src/Provers/splitter.ML";
     4.6  use "~~/src/Provers/hypsubst.ML";
     4.7 +use "~~/src/Provers/make_elim.ML";
     4.8  use "~~/src/Provers/classical.ML";
     4.9  use "~~/src/Provers/blast.ML";
    4.10  use "~~/src/Provers/clasimp.ML";