# HG changeset patch
# User paulson
# Date 1135163147 -3600
# Node ID 6e805f389355972dd29b6a99fe457d289144740d
# Parent  da548623916a260421d8b56fefb61c749cc9d1a0
modified suffix for [iff] attribute

diff -r da548623916a -r 6e805f389355 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Dec 21 12:02:57 2005 +0100
+++ b/src/Provers/clasimp.ML	Wed Dec 21 12:05:47 2005 +0100
@@ -141,7 +141,7 @@
   in
     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
            [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
-      handle THM _ => (elim (cs, [suffix_thm name "_iff" (zero_rotate (th RS Data.notE))])
+      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;