src/HOL/cladata.ML
changeset 10383 a092ae7bb2a6
parent 10231 178a272bceeb
child 10429 8820f787e61e
     1.1 --- a/src/HOL/cladata.ML	Fri Nov 03 21:29:56 2000 +0100
     1.2 +++ b/src/HOL/cladata.ML	Fri Nov 03 21:31:11 2000 +0100
     1.3 @@ -47,6 +47,7 @@
     1.4    val classical = classical
     1.5    val sizef     = size_of_thm
     1.6    val hyp_subst_tacs=[hyp_subst_tac]
     1.7 +  val atomize	= thms "atomize"
     1.8    end;
     1.9  
    1.10  structure Classical = ClassicalFun(Classical_Data);
    1.11 @@ -56,9 +57,6 @@
    1.12  
    1.13  bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
    1.14  
    1.15 -structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
    1.16 -  that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
    1.17 -
    1.18  (*Propositional rules*)
    1.19  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.20                         addSEs [conjE,disjE,impCE,FalseE,iffCE];