updated ObtainFun;
authorwenzelm
Sun Jul 30 13:01:50 2000 +0200 (2000-07-30)
changeset 9472b63b21f370ca
parent 9471 f778551af3ed
child 9473 7d13a5ace928
updated ObtainFun;
src/FOL/cladata.ML
src/HOL/cladata.ML
     1.1 --- a/src/FOL/cladata.ML	Sun Jul 30 13:01:09 2000 +0200
     1.2 +++ b/src/FOL/cladata.ML	Sun Jul 30 13:01:50 2000 +0200
     1.3 @@ -33,7 +33,8 @@
     1.4  
     1.5  structure Cla = ClassicalFun(Classical_Data);
     1.6  structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
     1.7 -structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
     1.8 +structure Obtain = ObtainFun(val atomic_thesis = FOLogic.atomic_Trueprop and
     1.9 +  that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
    1.10  
    1.11  
    1.12  (*Better for fast_tac: needs no quantifier duplication!*)
     2.1 --- a/src/HOL/cladata.ML	Sun Jul 30 13:01:09 2000 +0200
     2.2 +++ b/src/HOL/cladata.ML	Sun Jul 30 13:01:50 2000 +0200
     2.3 @@ -55,7 +55,8 @@
     2.4  
     2.5  structure Classical = ClassicalFun(Classical_Data);
     2.6  structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
     2.7 -structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
     2.8 +structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
     2.9 +  that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
    2.10  
    2.11  (*Propositional rules*)
    2.12  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]