# HG changeset patch
# User lcp
# Date 796608029 -7200
# Node ID 8317adb1c44449d62ef0ee12021431353b1bfa8f
# Parent  32bb5a8d5aab9e6581eaa5d36084e9e3e6d79d1e
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)

diff -r 32bb5a8d5aab -r 8317adb1c444 src/HOL/simpdata.ML
--- 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", []),