# HG changeset patch
# User paulson
# Date 840446704 -7200
# Node ID 27b71d839d5076c106110a057fb1bfde29a685ec
# Parent  43521f79f01698064f442d3e09503f25ea92527e
Added proof of Un_insert_right

diff -r 43521f79f016 -r 27b71d839d50 src/HOL/equalities.ML
--- 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";