Added insert_commute
authorpaulson
Mon Jul 22 16:24:47 1996 +0200 (1996-07-22)
changeset 187983c70ad381c1
parent 1878 ac8e534b4834
child 1880 78c4b3ddba6c
Added insert_commute
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Mon Jul 22 16:16:51 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Mon Jul 22 16:24:47 1996 +0200
     1.3 @@ -58,6 +58,10 @@
     1.4  qed "insert_absorb2";
     1.5  Addsimps [insert_absorb2];
     1.6  
     1.7 +goal Set.thy "insert x (insert y A) = insert y (insert x A)";
     1.8 +by (Fast_tac 1);
     1.9 +qed "insert_commute";
    1.10 +
    1.11  goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    1.12  by (Fast_tac 1);
    1.13  qed "insert_subset";