--- a/src/FOL/IsaMakefile Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/IsaMakefile Sat Dec 31 21:49:36 2005 +0100
@@ -32,9 +32,9 @@
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
- $(SRC)/Provers/make_elim.ML $(SRC)/Provers/project_rule.ML \
- $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.ML FOL.thy \
- FOL_lemmas1.ML IFOL.ML IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \
+ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
+ $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML \
+ IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \
document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML \
intprover.ML simpdata.ML
@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
--- a/src/FOL/ROOT.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/ROOT.ML Sat Dec 31 21:49:36 2005 +0100
@@ -12,7 +12,6 @@
use "~~/src/Provers/ind.ML";
use "~~/src/Provers/hypsubst.ML";
use "~~/src/Provers/induct_method.ML";
-use "~~/src/Provers/make_elim.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
use "~~/src/Provers/clasimp.ML";
--- a/src/FOL/cladata.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/cladata.ML Sat Dec 31 21:49:36 2005 +0100
@@ -8,17 +8,9 @@
section "Classical Reasoner";
-(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
-
-(*we don't redeclare the original make_elim (Tactic.make_elim) for
- compatibility with strange things done in many existing proofs *)
-val cla_make_elim = Make_Elim.make_elim;
-
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
- val make_elim = cla_make_elim
val mp = mp
val not_elim = notE
val classical = classical
--- a/src/FOL/simpdata.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/simpdata.ML Sat Dec 31 21:49:36 2005 +0100
@@ -369,8 +369,7 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
and Classical = Cla and Blast = Blast
- val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
- val cla_make_elim = cla_make_elim);
+ val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
open Clasimp;
val FOL_css = (FOL_cs, FOL_ss);
--- a/src/HOL/IsaMakefile Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/IsaMakefile Sat Dec 31 21:49:36 2005 +0100
@@ -71,8 +71,8 @@
$(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
- $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML \
- $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
+ $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \
+ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML \
$(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \
--- a/src/HOL/ROOT.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/ROOT.ML Sat Dec 31 21:49:36 2005 +0100
@@ -14,7 +14,6 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
use "~~/src/Provers/induct_method.ML";
-use "~~/src/Provers/make_elim.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
use "~~/src/Provers/clasimp.ML";
--- a/src/HOL/cladata.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/cladata.ML Sat Dec 31 21:49:36 2005 +0100
@@ -36,18 +36,9 @@
(List.nth (Thm.prems_of thm, i - 1)) then hyp_subst_tac i thm else no_tac thm;
-
-(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
-
-(*we don't redeclare the original make_elim (Tactic.make_elim) for
- compatibliity with strange things done in many existing proofs *)
-val cla_make_elim = Make_Elim.make_elim;
-
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
- val make_elim = cla_make_elim
val mp = mp
val not_elim = notE
val classical = classical
--- a/src/HOL/simpdata.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/HOL/simpdata.ML Sat Dec 31 21:49:36 2005 +0100
@@ -433,8 +433,7 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
and Classical = Classical and Blast = Blast
- val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
- val cla_make_elim = cla_make_elim);
+ val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
open Clasimp;
val HOL_css = (HOL_cs, HOL_ss);
--- a/src/Provers/clasimp.ML Sat Dec 31 21:49:35 2005 +0100
+++ b/src/Provers/clasimp.ML Sat Dec 31 21:49:36 2005 +0100
@@ -18,7 +18,6 @@
val notE: thm
val iffD1: thm
val iffD2: thm
- val cla_make_elim: thm -> thm
end
signature CLASIMP =
@@ -140,7 +139,7 @@
val zero_rotate = zero_var_indexes o rotate_prems n;
in
(elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
- [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
+ [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
handle THM _ => intro (cs, [th])),
simp (ss, [th]))
@@ -149,7 +148,7 @@
fun delIff delcs delss ((cs, ss), th) =
let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
(delcs (cs, [zero_rotate (th RS Data.iffD2),
- Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
+ Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
handle THM _ => delcs (cs, [th])),
delss (ss, [th]))