new theorem neq_commute
authorpaulson
Thu Aug 03 11:51:11 2000 +0200 (2000-08-03)
changeset 9511bb029080ff8b
parent 9510 dbcb1a6c92e1
child 9512 c30f6d0f81d2
new theorem neq_commute
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Aug 03 10:53:06 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Aug 03 11:51:11 2000 +0200
     1.3 @@ -190,11 +190,13 @@
     1.4  
     1.5  fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
     1.6  
     1.7 -prove "eq_commute" "(a=b)=(b=a)";
     1.8 +prove "eq_commute" "(a=b) = (b=a)";
     1.9  prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))";
    1.10  prove "eq_assoc" "((P=Q)=R) = (P=(Q=R))";
    1.11  val eq_ac = [eq_commute, eq_left_commute, eq_assoc];
    1.12  
    1.13 +prove "neq_commute" "(a~=b) = (b~=a)";
    1.14 +
    1.15  prove "conj_commute" "(P&Q) = (Q&P)";
    1.16  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
    1.17  val conj_comms = [conj_commute, conj_left_commute];