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