Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
The change from iffE to iffCE means fewer case splits in most cases. Very few
authorpaulson
Wed, 26 Nov 1997 17:31:02 +0100
changeset 4305 03d7de40ee4f
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 file | annotate | diff | comparison | revisions
src/HOL/cladata.ML file | annotate | diff | comparison | revisions 
--- 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] 
--- 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]
isabelle