author | nipkow |
Sat, 06 Aug 2005 08:16:19 +0200 | |
changeset 17026 | 43cc86fd3536 |
parent 17025 | b4a6b987aebe |
child 17027 | 8bbe57116d13 |
--- 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"