--- a/simpdata.ML Fri Jan 14 12:35:27 1994 +0100
+++ b/simpdata.ML Mon Jan 24 15:59:02 1994 +0100
@@ -67,6 +67,7 @@
in
+val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
val if_True = prove_goal HOL.thy "if(True,x,y) = x"
(fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
@@ -94,7 +95,7 @@
setmksimps mk_rews
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac)
setsubgoaler asm_simp_tac
- addsimps ([if_True, if_False, o_apply] @ simp_thms)
+ addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)
addcongs [imp_cong];
fun split_tac splits =