# HG changeset patch
# User lcp
# Date 796563576 -7200
# Node ID 90fc443e24ed30e6715f216b36c3a609280e01ad
# Parent  d24669439715977f9cb1f2efa2362d1ef5db862c
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)

diff -r d24669439715 -r 90fc443e24ed simpdata.ML
--- 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", []),