1.1 --- a/src/HOL/simpdata.ML	Thu Mar 30 14:07:52 1995 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 31 02:00:29 1995 +0200
     1.3 @@ -94,9 +94,14 @@
     1.4                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
     1.5                     (fn _ => [rtac expand_if 1]);
     1.6  
     1.7 -infix addcongs;
     1.8 +(*Add congruence rules for = (instead of ==) *)
     1.9 +infix 4 addcongs;
    1.10  fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    1.11  
    1.12 +(*Add a simpset to a classical set!*)
    1.13 +infix 4 addss;
    1.14 +fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    1.15 +
    1.16  val mksimps_pairs =
    1.17    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.18     ("All", [spec]), ("True", []), ("False", []),