--- 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", []),