changeset 17026 | 43cc86fd3536 |
parent 15391 | 797ed46d724b |
child 17084 | fb0a80aef0be |
--- 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"