# HG changeset patch
# User paulson
# Date 962181428 -7200
# Node ID 998dd2fb5795049ae850d42910994ce051415d25
# Parent  b9fe44ad3381e0bf533dfb13f09dda9b33976372
new file Provers/make_elim.ML

diff -r b9fe44ad3381 -r 998dd2fb5795 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Tue Jun 27 23:43:46 2000 +0200
+++ b/src/FOL/IsaMakefile	Wed Jun 28 10:37:08 2000 +0200
@@ -26,7 +26,7 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	\
+$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \
   $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \
diff -r b9fe44ad3381 -r 998dd2fb5795 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Tue Jun 27 23:43:46 2000 +0200
+++ b/src/FOL/ROOT.ML	Wed Jun 28 10:37:08 2000 +0200
@@ -16,6 +16,7 @@
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";
 use "~~/src/Provers/clasimp.ML";
diff -r b9fe44ad3381 -r 998dd2fb5795 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 27 23:43:46 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 28 10:37:08 2000 +0200
@@ -36,7 +36,8 @@
   $(SRC)/Provers/Arith/assoc_fold.ML		\
   $(SRC)/Provers/Arith/combine_numerals.ML	\
   $(SRC)/Provers/Arith/cancel_numerals.ML	\
-  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
+  $(SRC)/Provers/Arith/fast_lin_arith.ML \
+  $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
   $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
diff -r b9fe44ad3381 -r 998dd2fb5795 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Jun 27 23:43:46 2000 +0200
+++ b/src/HOL/ROOT.ML	Wed Jun 28 10:37:08 2000 +0200
@@ -20,6 +20,7 @@
 use "~~/src/Provers/split_paired_all.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";
 use "~~/src/Provers/clasimp.ML";