# HG changeset patch
# User lcp
# Date 796563360 -7200
# Node ID 864370666a241547dafbd64f936aafdd25632629
# Parent  33e3054b2871154b1387a10a4a2e3e54be30bbc7
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)

diff -r 33e3054b2871 -r 864370666a24 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Mar 30 13:07:59 1995 +0200
+++ b/src/FOL/simpdata.ML	Thu Mar 30 13:36:00 1995 +0200
@@ -90,10 +90,16 @@
 
 open Simplifier Induction;
 
-infix addcongs;
+(*Add congruence rules for = or <-> (instead of ==) *)
+infix 4 addcongs;
 fun ss addcongs congs =
     ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
 
+(*Add a simpset to a classical set!*)
+infix 4 addss;
+fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
+
+
 val IFOL_rews =
    [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
     imp_rews @ iff_rews @ quant_rews;