removed obsolete Provers/make_elim.ML;
authorwenzelm
Sat Dec 31 21:49:36 2005 +0100 (2005-12-31 ago)
changeset 18529540da2415751
parent 18528 85e7f80023fc
child 18530 d995aecddc15
removed obsolete Provers/make_elim.ML;
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/FOL/cladata.ML
src/FOL/simpdata.ML
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/cladata.ML
src/HOL/simpdata.ML
src/Provers/clasimp.ML
     1.1 --- a/src/FOL/IsaMakefile	Sat Dec 31 21:49:35 2005 +0100
     1.2 +++ b/src/FOL/IsaMakefile	Sat Dec 31 21:49:36 2005 +0100
     1.3 @@ -32,9 +32,9 @@
     1.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
     1.5    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
     1.6    $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML			\
     1.7 -  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/project_rule.ML            \
     1.8 -  $(SRC)/Provers/quantifier1.ML	$(SRC)/Provers/splitter.ML FOL.ML FOL.thy \
     1.9 -  FOL_lemmas1.ML IFOL.ML IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \
    1.10 +  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    1.11 +  $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML	\
    1.12 +  IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML 		\
    1.13    document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML	\
    1.14    intprover.ML simpdata.ML
    1.15  	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
     2.1 --- a/src/FOL/ROOT.ML	Sat Dec 31 21:49:35 2005 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Sat Dec 31 21:49:36 2005 +0100
     2.3 @@ -12,7 +12,6 @@
     2.4  use "~~/src/Provers/ind.ML";
     2.5  use "~~/src/Provers/hypsubst.ML";
     2.6  use "~~/src/Provers/induct_method.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/FOL/cladata.ML	Sat Dec 31 21:49:35 2005 +0100
     3.2 +++ b/src/FOL/cladata.ML	Sat Dec 31 21:49:36 2005 +0100
     3.3 @@ -8,17 +8,9 @@
     3.4  
     3.5  section "Classical Reasoner";
     3.6  
     3.7 -(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     3.8 -structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
     3.9 -
    3.10 -(*we don't redeclare the original make_elim (Tactic.make_elim) for 
    3.11 -  compatibility with strange things done in many existing proofs *)
    3.12 -val cla_make_elim = Make_Elim.make_elim;
    3.13 -
    3.14  (*** Applying ClassicalFun to create a classical prover ***)
    3.15  structure Classical_Data = 
    3.16    struct
    3.17 -  val make_elim = cla_make_elim
    3.18    val mp        = mp
    3.19    val not_elim  = notE
    3.20    val classical = classical
     4.1 --- a/src/FOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
     4.2 +++ b/src/FOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
     4.3 @@ -369,8 +369,7 @@
     4.4  structure Clasimp = ClasimpFun
     4.5   (structure Simplifier = Simplifier and Splitter = Splitter
     4.6    and Classical  = Cla and Blast = Blast
     4.7 -  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
     4.8 -  val cla_make_elim = cla_make_elim);
     4.9 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
    4.10  open Clasimp;
    4.11  
    4.12  val FOL_css = (FOL_cs, FOL_ss);
     5.1 --- a/src/HOL/IsaMakefile	Sat Dec 31 21:49:35 2005 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Sat Dec 31 21:49:36 2005 +0100
     5.3 @@ -71,8 +71,8 @@
     5.4    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML		\
     5.5    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML				\
     5.6    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML				\
     5.7 -  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML			\
     5.8 -  $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
     5.9 +  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML			\
    5.10 +  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
    5.11    $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML	\
    5.12    $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
    5.13    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
     6.1 --- a/src/HOL/ROOT.ML	Sat Dec 31 21:49:35 2005 +0100
     6.2 +++ b/src/HOL/ROOT.ML	Sat Dec 31 21:49:36 2005 +0100
     6.3 @@ -14,7 +14,6 @@
     6.4  use "~~/src/Provers/splitter.ML";
     6.5  use "~~/src/Provers/hypsubst.ML";
     6.6  use "~~/src/Provers/induct_method.ML";
     6.7 -use "~~/src/Provers/make_elim.ML";
     6.8  use "~~/src/Provers/classical.ML";
     6.9  use "~~/src/Provers/blast.ML";
    6.10  use "~~/src/Provers/clasimp.ML";
     7.1 --- a/src/HOL/cladata.ML	Sat Dec 31 21:49:35 2005 +0100
     7.2 +++ b/src/HOL/cladata.ML	Sat Dec 31 21:49:36 2005 +0100
     7.3 @@ -36,18 +36,9 @@
     7.4      (List.nth (Thm.prems_of thm, i - 1)) then hyp_subst_tac i thm else no_tac thm;
     7.5  
     7.6  
     7.7 -
     7.8 -(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     7.9 -structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
    7.10 -
    7.11 -(*we don't redeclare the original make_elim (Tactic.make_elim) for 
    7.12 -  compatibliity with strange things done in many existing proofs *)
    7.13 -val cla_make_elim = Make_Elim.make_elim;
    7.14 -
    7.15  (*** Applying ClassicalFun to create a classical prover ***)
    7.16  structure Classical_Data = 
    7.17    struct
    7.18 -  val make_elim = cla_make_elim
    7.19    val mp        = mp
    7.20    val not_elim  = notE
    7.21    val classical = classical
     8.1 --- a/src/HOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
     8.2 +++ b/src/HOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
     8.3 @@ -433,8 +433,7 @@
     8.4  structure Clasimp = ClasimpFun
     8.5   (structure Simplifier = Simplifier and Splitter = Splitter
     8.6    and Classical  = Classical and Blast = Blast
     8.7 -  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
     8.8 -  val cla_make_elim = cla_make_elim);
     8.9 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
    8.10  open Clasimp;
    8.11  
    8.12  val HOL_css = (HOL_cs, HOL_ss);
     9.1 --- a/src/Provers/clasimp.ML	Sat Dec 31 21:49:35 2005 +0100
     9.2 +++ b/src/Provers/clasimp.ML	Sat Dec 31 21:49:36 2005 +0100
     9.3 @@ -18,7 +18,6 @@
     9.4    val notE: thm
     9.5    val iffD1: thm
     9.6    val iffD2: thm
     9.7 -  val cla_make_elim: thm -> thm
     9.8  end
     9.9  
    9.10  signature CLASIMP =
    9.11 @@ -140,7 +139,7 @@
    9.12      val zero_rotate = zero_var_indexes o rotate_prems n;
    9.13    in
    9.14      (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
    9.15 -           [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
    9.16 +           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
    9.17        handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
    9.18          handle THM _ => intro (cs, [th])),
    9.19       simp (ss, [th]))
    9.20 @@ -149,7 +148,7 @@
    9.21  fun delIff delcs delss ((cs, ss), th) =
    9.22    let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    9.23      (delcs (cs, [zero_rotate (th RS Data.iffD2),
    9.24 -        Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
    9.25 +        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
    9.26        handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
    9.27          handle THM _ => delcs (cs, [th])),
    9.28       delss (ss, [th]))