declaring and using cla_make_elim
authorpaulson
Wed Jun 28 10:37:52 2000 +0200 (2000-06-28)
changeset 9158084abf3d0eff
parent 9157 998dd2fb5795
child 9159 902ea754eee2
declaring and using cla_make_elim
src/FOL/cladata.ML
src/HOL/cladata.ML
     1.1 --- a/src/FOL/cladata.ML	Wed Jun 28 10:37:08 2000 +0200
     1.2 +++ b/src/FOL/cladata.ML	Wed Jun 28 10:37:52 2000 +0200
     1.3 @@ -8,14 +8,26 @@
     1.4  
     1.5  section "Classical Reasoner";
     1.6  
     1.7 +(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     1.8 +structure Make_Elim_Data =
     1.9 +struct
    1.10 +  val classical = classical
    1.11 +end;
    1.12 +
    1.13 +structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
    1.14 +
    1.15 +(*we don't redeclare the original make_elim (Tactic.make_elim) for 
    1.16 +  compatibliity with strange things done in many existing proofs *)
    1.17 +val cla_make_elim = Make_Elim.make_elim;
    1.18  
    1.19  (*** Applying ClassicalFun to create a classical prover ***)
    1.20  structure Classical_Data = 
    1.21    struct
    1.22 -  val sizef     = size_of_thm
    1.23 +  val make_elim = cla_make_elim
    1.24    val mp        = mp
    1.25    val not_elim  = notE
    1.26    val classical = classical
    1.27 +  val sizef     = size_of_thm
    1.28    val hyp_subst_tacs=[hyp_subst_tac]
    1.29    end;
    1.30  
     2.1 --- a/src/HOL/cladata.ML	Wed Jun 28 10:37:08 2000 +0200
     2.2 +++ b/src/HOL/cladata.ML	Wed Jun 28 10:37:52 2000 +0200
     2.3 @@ -29,13 +29,27 @@
     2.4  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     2.5  open Hypsubst;
     2.6  
     2.7 +
     2.8 +(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     2.9 +structure Make_Elim_Data =
    2.10 +struct
    2.11 +  val classical = classical
    2.12 +end;
    2.13 +
    2.14 +structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
    2.15 +
    2.16 +(*we don't redeclare the original make_elim (Tactic.make_elim) for 
    2.17 +  compatibliity with strange things done in many existing proofs *)
    2.18 +val cla_make_elim = Make_Elim.make_elim;
    2.19 +
    2.20  (*** Applying ClassicalFun to create a classical prover ***)
    2.21  structure Classical_Data = 
    2.22    struct
    2.23 -  val sizef     = size_of_thm
    2.24 +  val make_elim = cla_make_elim
    2.25    val mp        = mp
    2.26    val not_elim  = notE
    2.27    val classical = classical
    2.28 +  val sizef     = size_of_thm
    2.29    val hyp_subst_tacs=[hyp_subst_tac]
    2.30    end;
    2.31