# HG changeset patch
# User paulson
# Date 880561862 -3600
# Node ID 03d7de40ee4fe56d143524be4335cc01b8d89957
# Parent  af2a2cd9fa512e592f7e630e362661fe02dadf0a
The change from iffE to iffCE means fewer case splits in most cases.  Very few
proofs are affected, almost none adversely

diff -r af2a2cd9fa51 -r 03d7de40ee4f src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Nov 26 17:27:34 1997 +0100
+++ b/src/FOL/cladata.ML	Wed Nov 26 17:31:02 1997 +0100
@@ -35,11 +35,9 @@
     (IntPr.fast_tac 1)]);
 
 
-(*Propositional rules 
-  -- iffCE might seem better, but in the examples in ex/cla
-     run about 7% slower than with iffE*)
+(*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
-                       addSEs [conjE,disjE,impCE,FalseE,iffE];
+                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
diff -r af2a2cd9fa51 -r 03d7de40ee4f src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Nov 26 17:27:34 1997 +0100
+++ b/src/HOL/cladata.ML	Wed Nov 26 17:31:02 1997 +0100
@@ -43,7 +43,7 @@
 
 (*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
-                       addSEs [conjE,disjE,impCE,FalseE,iffE];
+                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
 val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]