# HG changeset patch
# User paulson
# Date 997094781 -7200
# Node ID cf3e7f5ad0e1d0e98fe0fef741ea85fc44d9c1b3
# Parent  ffeac9aa1967bd9b3fd94840411811f8afedb296
removed the warning from [iff]

diff -r ffeac9aa1967 -r cf3e7f5ad0e1 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon Aug 06 12:42:43 2001 +0200
+++ b/src/Provers/clasimp.ML	Mon Aug 06 12:46:21 2001 +0200
@@ -117,25 +117,21 @@
         the Safe Intr     rule B==>A and
         the Safe Destruct rule A==>B.
   Also ~A goes to the Safe Elim rule A ==> ?R
-  Failing other cases, A is added as a Safe Intr rule and a warning is issued *)
+  Failing other cases, A is added as a Safe Intr rule*)
 local
 
 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)])
-   handle THM _ => (warning ("iff add: theorem is not an equivalence\n" 
-                  ^ Display.string_of_thm th);
-                    elim (cs, [zero_var_indexes (th RS Data.notE )])
-   handle THM _ => intro (cs, [th])),
+   handle THM _ => (elim (cs, [zero_var_indexes (th RS Data.notE )])
+                    handle THM _ => intro (cs, [th])),
    simp (ss, [th]));
 
 fun delIff ((cs, ss), th) =
-(                Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
-                      Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
- handle THM _ => (warning ("iff del: theorem is not an equivalence\n" 
-                  ^ Display.string_of_thm th);
-                 Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
- handle THM _ => Classical.delrules (cs, [th])), 
+(             Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
+                   Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
+ handle THM _ => (Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
+                  handle THM _ => Classical.delrules (cs, [th])), 
  Simplifier.delsimps (ss, [th]));
 
 fun store_clasimp (cs, ss) =