src/HOL/Sum_Type.thy

--- a/src/HOL/Sum_Type.thy	Fri Aug 05 19:58:30 2005 +0200
+++ b/src/HOL/Sum_Type.thy	Sat Aug 06 08:16:19 2005 +0200
@@ -151,6 +151,14 @@
 by (rule sumE [of x], auto)
 
 
+lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
+apply (rule set_ext)
+apply(rename_tac s)
+apply(rule_tac s=s in sumE)
+apply auto
+done
+
+
 subsection{*The @{term Part} Primitive*}
 
 lemma Part_eqI [intro]: "[| a : A;  a=h(b) |] ==> a : Part A h"