Added proof of Un_insert_right

--- a/src/HOL/equalities.ML	Mon Aug 19 11:23:25 1996 +0200
+++ b/src/HOL/equalities.ML	Mon Aug 19 11:25:04 1996 +0200
@@ -211,6 +211,10 @@
 by (Fast_tac 1);
 qed "Un_insert_left";
 
+goal Set.thy "A Un (insert a B) = insert a (A Un B)";
+by (Fast_tac 1);
+qed "Un_insert_right";
+
 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (Fast_tac 1);
 qed "Un_Int_distrib";