--- 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]