src/HOL/cladata.ML
changeset 10906 de95ba2760fe
parent 10429 8820f787e61e
child 11440 e389e4338604
     1.1 --- a/src/HOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
     1.2 +++ b/src/HOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
     1.3 @@ -38,6 +38,10 @@
     1.4    compatibliity with strange things done in many existing proofs *)
     1.5  val cla_make_elim = Make_Elim.make_elim;
     1.6  
     1.7 +val atomize_rules = thms "atomize'";
     1.8 +val atomize_tac = Method.atomize_tac atomize_rules;
     1.9 +val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
    1.10 +
    1.11  (*** Applying ClassicalFun to create a classical prover ***)
    1.12  structure Classical_Data = 
    1.13    struct
    1.14 @@ -47,7 +51,7 @@
    1.15    val classical = classical
    1.16    val sizef     = size_of_thm
    1.17    val hyp_subst_tacs=[hyp_subst_tac]
    1.18 -  val atomize	= thms "atomize'"
    1.19 +  val atomize	= atomize_rules
    1.20    end;
    1.21  
    1.22  structure Classical = ClassicalFun(Classical_Data);