# HG changeset patch
# User wenzelm
# Date 954532836 -7200
# Node ID 978db2870862e1e23a06b1ab7471b5c877d5347a
# Parent  2f9b008a27a1aac4fd08d85dfd149b8304b01957
change_global/local_css move to Provers/clasimp.ML;
fixed 'iff' att syntax;
added 'cong' att;

diff -r 2f9b008a27a1 -r 978db2870862 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Mar 31 21:59:37 2000 +0200
+++ b/src/HOL/simpdata.ML	Fri Mar 31 22:00:36 2000 +0200
@@ -57,38 +57,6 @@
 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 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")]];
-
-end;
-
-
 val [prem] = goal (the_context ()) "x==y ==> x=y";
 by (rewtac prem);
 by (rtac refl 1);
@@ -155,6 +123,13 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
+val cong_add_global = Simplifier.change_global_ss (op addcongs);
+val cong_add_local = Simplifier.change_local_ss (op addcongs);
+
+val cong_attrib_setup =
+  [Attrib.add_attributes [("cong", (Attrib.no_args cong_add_global, Attrib.no_args cong_add_local),
+    "add rules to simpset and claset simultaneously")]];
+
 
 val imp_cong = impI RSN
     (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
@@ -524,6 +499,17 @@
 val HOL_css = (HOL_cs, HOL_ss);
 
 
+(* "iff" attribute *)
+
+val iff_add_global = Clasimp.change_global_css (op addIffs);
+val iff_add_local = Clasimp.change_local_css (op addIffs);
+
+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")]];
+
+
+
 (*** A general refutation procedure ***)
  
 (* Parameters: