# HG changeset patch
# User oheimb
# Date 997378402 -7200
# Node ID fa8d12b789e12a5ce595962ddb4ffa45935f570c
# Parent  3621dea6113e71603426b2c6b90b3944b934b25a
corrected semantics of [iff] concerning rules with premises

diff -r 3621dea6113e -r fa8d12b789e1 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Aug 09 18:51:41 2001 +0200
+++ b/src/Provers/clasimp.ML	Thu Aug 09 19:33:22 2001 +0200
@@ -122,7 +122,8 @@
 
 fun addIff dest elim intro simp ((cs, ss), th) =
   (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
-                              [zero_var_indexes (th RS Data.iffD1)])
+                              [zero_var_indexes (rotate_prems (nprems_of th)
+                                                (th RS Data.iffD1))])
    handle THM _ => (elim (cs, [zero_var_indexes (th RS Data.notE )])
                     handle THM _ => intro (cs, [th])),
    simp (ss, [th]));