# HG changeset patch
# User wenzelm
# Date 967924070 -7200
# Node ID 5e7c4a45d8bbd0ad07fed51581c9e197d2509da2
# Parent  221388d5696d8b3fac77bc460d93ef95df60e02c
added 'iff del' att;

diff -r 221388d5696d -r 5e7c4a45d8bb src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Sep 02 21:47:21 2000 +0200
+++ b/src/HOL/simpdata.ML	Sat Sep 02 21:47:50 2000 +0200
@@ -525,11 +525,15 @@
 (* "iff" attribute *)
 
 val iff_add_global = Clasimp.change_global_css (op addIffs);
+val iff_del_global = Clasimp.change_global_css (op delIffs);
 val iff_add_local = Clasimp.change_local_css (op addIffs);
+val iff_del_local = Clasimp.change_local_css (op delIffs);
 
 val iff_attrib_setup =
-  [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
-    "add rules to simpset and claset simultaneously")]];
+ [Attrib.add_attributes
+  [("iff", (Attrib.add_del_args iff_add_global iff_del_global,
+    Attrib.add_del_args iff_add_local iff_del_local),
+    "declare simplifier / classical rules")]];