--- a/simpdata.ML	Tue Mar 28 12:48:46 1995 +0200
+++ b/simpdata.ML	Thu Mar 30 13:39:36 1995 +0200
@@ -93,9 +93,14 @@
 val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))"
   (fn _ => [rtac expand_if 1]);
 
-infix addcongs;
+(*Add congruence rules for = (instead of ==) *)
+infix 4 addcongs;
 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
 
+(*Add a simpset to a classical set!*)
+infix 4 addss;
+fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
+
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),