"iff" attribute;
simpdata_setup;

--- a/src/HOL/simpdata.ML	Tue Apr 27 10:43:52 1999 +0200
+++ b/src/HOL/simpdata.ML	Tue Apr 27 10:44:17 1999 +0200
@@ -8,7 +8,7 @@
 
 section "Simplifier";
 
-(*** Addition of rules to simpsets and clasets simultaneously ***)
+(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
 
 infix 4 addIffs delIffs;
 
@@ -57,6 +57,38 @@
 end;
 
 
+(* "iff" attribute *)
+
+local
+  fun change_global_css f (thy, th) =
+    let
+      val cs_ref = Classical.claset_ref_of thy;
+      val ss_ref = Simplifier.simpset_ref_of thy;
+      val (cs', ss') = f ((! cs_ref, ! ss_ref), [th]);
+    in cs_ref := cs'; ss_ref := ss'; (thy, th) end;
+
+  fun change_local_css f (ctxt, th) =
+    let
+      val cs = Classical.get_local_claset ctxt;
+      val ss = Simplifier.get_local_simpset ctxt;
+      val (cs', ss') = f ((cs, ss), [th]);
+      val ctxt' =
+        ctxt
+        |> Classical.put_local_claset cs'
+        |> Simplifier.put_local_simpset ss';
+    in (ctxt', th) end;
+in
+
+val iff_add_global = change_global_css (op addIffs);
+val iff_add_local = change_local_css (op addIffs);
+
+val simpdata_setup =
+  [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
+    "add rules to simpset and claset simultaneously")]];
+
+end;
+
+
 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);