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.
Fixed delIffs to deal correctly with the D-rule
authorpaulson
Mon, 14 Jul 1997 12:44:09 +0200
changeset 3518 6e11c7bfb9c7
parent 3517 2547f33fa33a
child 3519 ab0a9fbed4c0
Fixed delIffs to deal correctly with the D-rule
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/simpdata.ML	Mon Jul 14 12:42:28 1997 +0200
+++ b/src/HOL/simpdata.ML	Mon Jul 14 12:44:09 1997 +0200
@@ -41,7 +41,7 @@
               | (con $ _ $ _) =>
                     if con=iff_const
                     then Delrules [zero_var_indexes (th RS iffD2),
-                                   zero_var_indexes (th RS iffD1)]
+                                   make_elim (zero_var_indexes (th RS iffD1))]
                     else Delrules [th]
               | _ => Delrules [th];
        Delsimps [th])
isabelle