eliminated atomize rules;
authorwenzelm
Sun Oct 14 19:59:55 2001 +0200 (2001-10-14 ago)
changeset 1174806eb315831ff
parent 11747 17a6dcd6f3cf
child 11749 fc8afdc58b26
eliminated atomize rules;
src/FOL/blastdata.ML
src/FOL/cladata.ML
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/blastdata.ML	Sun Oct 14 19:59:15 2001 +0200
     1.2 +++ b/src/FOL/blastdata.ML	Sun Oct 14 19:59:55 2001 +0200
     1.3 @@ -10,7 +10,6 @@
     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	= atomize_rules
     1.8    val cla_modifiers = Cla.cla_modifiers;
     1.9    val cla_meth' = Cla.cla_meth'
    1.10    end;
     2.1 --- a/src/FOL/cladata.ML	Sun Oct 14 19:59:15 2001 +0200
     2.2 +++ b/src/FOL/cladata.ML	Sun Oct 14 19:59:55 2001 +0200
     2.3 @@ -15,10 +15,6 @@
     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 @@ -28,7 +24,6 @@
    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	= atomize_rules
    2.19    end;
    2.20  
    2.21  structure Cla = ClassicalFun(Classical_Data);
     3.1 --- a/src/FOL/simpdata.ML	Sun Oct 14 19:59:15 2001 +0200
     3.2 +++ b/src/FOL/simpdata.ML	Sun Oct 14 19:59:55 2001 +0200
     3.3 @@ -369,7 +369,8 @@
     3.4  (* rulify setup *)
     3.5  
     3.6  local
     3.7 -  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
     3.8 +  val ss = FOL_basic_ss addsimps
     3.9 +    [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
    3.10  in
    3.11  
    3.12  structure Rulify = RulifyFun