Added insert_commute

--- a/src/HOL/equalities.ML	Mon Jul 22 16:16:51 1996 +0200
+++ b/src/HOL/equalities.ML	Mon Jul 22 16:24:47 1996 +0200
@@ -58,6 +58,10 @@
 qed "insert_absorb2";
 Addsimps [insert_absorb2];
 
+goal Set.thy "insert x (insert y A) = insert y (insert x A)";
+by (Fast_tac 1);
+qed "insert_commute";
+
 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
 by (Fast_tac 1);
 qed "insert_subset";