diff -r 70d46a081b47 -r 7d437bed7765 simpdata.ML
--- 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 =