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