src/HOL/equalities.ML
changeset 1879 83c70ad381c1
parent 1843 a6d7aef48c2f
child 1884 5a1f81da3e12
     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";