--- 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;