The change from iffE to iffCE means fewer case splits in most cases. Very few
authorpaulson
Wed Nov 26 17:31:02 1997 +0100 (1997-11-26)
changeset 430503d7de40ee4f
parent 4304 af2a2cd9fa51
child 4306 ddbe1a9722ab
The change from iffE to iffCE means fewer case splits in most cases. Very few
proofs are affected, almost none adversely
src/FOL/cladata.ML
src/HOL/cladata.ML
     1.1 --- a/src/FOL/cladata.ML	Wed Nov 26 17:27:34 1997 +0100
     1.2 +++ b/src/FOL/cladata.ML	Wed Nov 26 17:31:02 1997 +0100
     1.3 @@ -35,11 +35,9 @@
     1.4      (IntPr.fast_tac 1)]);
     1.5  
     1.6  
     1.7 -(*Propositional rules 
     1.8 -  -- iffCE might seem better, but in the examples in ex/cla
     1.9 -     run about 7% slower than with iffE*)
    1.10 +(*Propositional rules*)
    1.11  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    1.12 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.13 +                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
    1.14  
    1.15  (*Quantifier rules*)
    1.16  val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
     2.1 --- a/src/HOL/cladata.ML	Wed Nov 26 17:27:34 1997 +0100
     2.2 +++ b/src/HOL/cladata.ML	Wed Nov 26 17:31:02 1997 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4  
     2.5  (*Propositional rules*)
     2.6  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
     2.7 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
     2.8 +                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
     2.9  
    2.10  (*Quantifier rules*)
    2.11  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]