# HG changeset patch
# User nipkow
# Date 1123308979 -7200
# Node ID 43cc86fd35369688b23efd1d97e7400660b78bd2
# Parent  b4a6b987aebed6e6cad0d70b6f1141a04099f400
new lemma

diff -r b4a6b987aebe -r 43cc86fd3536 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"