# HG changeset patch
# User paulson
# Date 938524370 -7200
# Node ID 23efbb7ab88974ef4f5636229f059a25590880d8
# Parent  dcb93b29568303c75c36666c3b30a3834ffe8d68
AC rules for equality

diff -r dcb93b295683 -r 23efbb7ab889 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Sep 28 15:12:27 1999 +0200
+++ b/src/HOL/simpdata.ML	Tue Sep 28 15:12:50 1999 +0200
@@ -202,6 +202,11 @@
 
 fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
 
+prove "eq_commute" "(a=b)=(b=a)";
+prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))";
+prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))";
+val eq_ac = [eq_commute, eq_left_commute, eq_assoc];
+
 prove "conj_commute" "(P&Q) = (Q&P)";
 prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
 val conj_comms = [conj_commute, conj_left_commute];