| changeset 40271 | 6014e8252e57 |
| parent 39302 | d7728f65b353 |
| child 40610 | 70776ecfe324 |
--- a/src/HOL/Sum_Type.thy Fri Oct 29 16:04:35 2010 +0200 +++ b/src/HOL/Sum_Type.thy Fri Oct 29 17:25:22 2010 +0200 @@ -162,6 +162,8 @@ definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where "A <+> B = Inl ` A \<union> Inr ` B" +hide_const (open) Plus --"Valuable identifier" + lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B" by (simp add: Plus_def)