Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)

--- a/src/HOL/simpdata.ML	Thu Mar 30 14:07:52 1995 +0200
+++ b/src/HOL/simpdata.ML	Fri Mar 31 02:00:29 1995 +0200
@@ -94,9 +94,14 @@
                    "(if P then Q else 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", []),