tuned atomize;
authorwenzelm
Tue Jan 16 00:28:50 2001 +0100 (2001-01-16)
changeset 10906de95ba2760fe
parent 10905 e23abeef8150
child 10907 51be80fc4439
tuned atomize;
src/FOL/blastdata.ML
src/FOL/cladata.ML
src/HOL/arith_data.ML
src/HOL/blastdata.ML
src/HOL/cladata.ML
     1.1 --- a/src/FOL/blastdata.ML	Tue Jan 16 00:27:37 2001 +0100
     1.2 +++ b/src/FOL/blastdata.ML	Tue Jan 16 00:28:50 2001 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     1.5    val claset	= Cla.claset
     1.6    val rep_cs    = Cla.rep_cs
     1.7 -  val atomize	= thms "atomize'"
     1.8 +  val atomize	= atomize_rules
     1.9    val cla_modifiers = Cla.cla_modifiers;
    1.10    val cla_meth' = Cla.cla_meth'
    1.11    end;
     2.1 --- a/src/FOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
     2.2 +++ b/src/FOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
     2.3 @@ -15,6 +15,10 @@
     2.4    compatibliity with strange things done in many existing proofs *)
     2.5  val cla_make_elim = Make_Elim.make_elim;
     2.6  
     2.7 +val atomize_rules = thms "atomize'";
     2.8 +val atomize_tac = Method.atomize_tac atomize_rules;
     2.9 +val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
    2.10 +
    2.11  (*** Applying ClassicalFun to create a classical prover ***)
    2.12  structure Classical_Data = 
    2.13    struct
    2.14 @@ -24,7 +28,7 @@
    2.15    val classical = classical
    2.16    val sizef     = size_of_thm
    2.17    val hyp_subst_tacs=[hyp_subst_tac]
    2.18 -  val atomize	= thms "atomize'"
    2.19 +  val atomize	= atomize_rules
    2.20    end;
    2.21  
    2.22  structure Cla = ClassicalFun(Classical_Data);
     3.1 --- a/src/HOL/arith_data.ML	Tue Jan 16 00:27:37 2001 +0100
     3.2 +++ b/src/HOL/arith_data.ML	Tue Jan 16 00:28:50 2001 +0100
     3.3 @@ -407,8 +407,6 @@
     3.4  *)
     3.5  local
     3.6  
     3.7 -val atomize_tac = Method.atomize_tac (thms "atomize'");
     3.8 -
     3.9  fun raw_arith_tac i st =
    3.10    refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    3.11               ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
     4.1 --- a/src/HOL/blastdata.ML	Tue Jan 16 00:27:37 2001 +0100
     4.2 +++ b/src/HOL/blastdata.ML	Tue Jan 16 00:28:50 2001 +0100
     4.3 @@ -23,7 +23,7 @@
     4.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     4.5    val claset	= Classical.claset
     4.6    val rep_cs    = Classical.rep_cs
     4.7 -  val atomize	= thms "atomize'"
     4.8 +  val atomize	= atomize_rules
     4.9    val cla_modifiers = Classical.cla_modifiers;
    4.10    val cla_meth' = Classical.cla_meth'
    4.11    end;
     5.1 --- a/src/HOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
     5.2 +++ b/src/HOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
     5.3 @@ -38,6 +38,10 @@
     5.4    compatibliity with strange things done in many existing proofs *)
     5.5  val cla_make_elim = Make_Elim.make_elim;
     5.6  
     5.7 +val atomize_rules = thms "atomize'";
     5.8 +val atomize_tac = Method.atomize_tac atomize_rules;
     5.9 +val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
    5.10 +
    5.11  (*** Applying ClassicalFun to create a classical prover ***)
    5.12  structure Classical_Data = 
    5.13    struct
    5.14 @@ -47,7 +51,7 @@
    5.15    val classical = classical
    5.16    val sizef     = size_of_thm
    5.17    val hyp_subst_tacs=[hyp_subst_tac]
    5.18 -  val atomize	= thms "atomize'"
    5.19 +  val atomize	= atomize_rules
    5.20    end;
    5.21  
    5.22  structure Classical = ClassicalFun(Classical_Data);