# HG changeset patch
# User paulson
# Date 965296271 -7200
# Node ID bb029080ff8b72489948e6a5f3f3819876a11868
# Parent  dbcb1a6c92e17725c6c7c32fc1a85c25186a9c3b
new theorem neq_commute

diff -r dbcb1a6c92e1 -r bb029080ff8b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Aug 03 10:53:06 2000 +0200
+++ b/src/HOL/simpdata.ML	Thu Aug 03 11:51:11 2000 +0200
@@ -190,11 +190,13 @@
 
 fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
 
-prove "eq_commute" "(a=b)=(b=a)";
+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 "neq_commute" "(a~=b) = (b~=a)";
+
 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];