diff -r ab88297f1a56 -r 32a83e3ad5a4 simpdata.ML
--- a/simpdata.ML	Tue Mar 22 19:55:29 1994 +0100
+++ b/simpdata.ML	Sun Mar 27 12:36:39 1994 +0200
@@ -70,8 +70,8 @@
 
 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
 val conj_commute = prover "(P&Q) = (Q&P)";
-val conj_right_commute = prover "((P&Q)&R) = ((P&R)&Q)";
-val conj_ac = [conj_assoc RS sym, conj_commute, conj_right_commute];
+val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
+val conj_comms = [conj_commute, conj_left_commute];
 
 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]);