src/HOL/Sum_Type.thy
changeset 17026 43cc86fd3536
parent 15391 797ed46d724b
child 17084 fb0a80aef0be
     1.1 --- a/src/HOL/Sum_Type.thy	Fri Aug 05 19:58:30 2005 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Sat Aug 06 08:16:19 2005 +0200
     1.3 @@ -151,6 +151,14 @@
     1.4  by (rule sumE [of x], auto)
     1.5  
     1.6  
     1.7 +lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
     1.8 +apply (rule set_ext)
     1.9 +apply(rename_tac s)
    1.10 +apply(rule_tac s=s in sumE)
    1.11 +apply auto
    1.12 +done
    1.13 +
    1.14 +
    1.15  subsection{*The @{term Part} Primitive*}
    1.16  
    1.17  lemma Part_eqI [intro]: "[| a : A;  a=h(b) |] ==> a : Part A h"