diff -r c5cda71de65d -r ee5c9672d208 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jul 13 11:44:02 2000 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 13 12:56:42 2000 +0200
@@ -6,6 +6,50 @@
 Simplification data for FOL
 *)
 
+(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
+
+infix 4 addIffs delIffs;
+
+(*Takes UNCONDITIONAL theorems of the form A<->B to 
+        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*)
+local
+  fun addIff ((cla, simp), th) = 
+      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
+                (Const("Not", _) $ A) =>
+                    cla addSEs [zero_var_indexes (th RS notE)]
+              | (Const("op <->", _) $ _ $ _) =>
+                    cla addSIs [zero_var_indexes (th RS iffD2)]  
+                        addSDs [zero_var_indexes (th RS iffD1)]
+              | _ => cla addSIs [th],
+       simp addsimps [th])
+      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
+                         string_of_thm th);
+
+  fun delIff ((cla, simp), th) = 
+      (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
+	   (Const ("Not", _) $ A) =>
+	       cla delrules [zero_var_indexes (th RS notE)]
+	 | (Const("op <->", _) $ _ $ _) =>
+	       cla delrules [zero_var_indexes (th RS iffD2),
+			     cla_make_elim (zero_var_indexes (th RS iffD1))]
+	 | _ => cla delrules [th],
+       simp delsimps [th])
+      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
+				string_of_thm th); (cla, simp));
+
+  fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
+in
+val op addIffs = foldl addIff;
+val op delIffs = foldl delIff;
+fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
+fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
+end;
+
+
+
 (* Elimination of True from asumptions: *)
 
 val True_implies_equals = prove_goal IFOL.thy