simpdata.ML

--- a/simpdata.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/simpdata.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -69,6 +69,9 @@
 in
 
 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 if_True = prove_goal HOL.thy "if(True,x,y) = x"
  (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);