src/HOL/Sum_Type.thy
changeset 45694 4a8743618257
parent 45204 5e4a1270c000
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Sum_Type.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -17,8 +17,10 @@
     1.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
     1.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
     1.6  
     1.7 -typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
     1.8 -  by auto
     1.9 +definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    1.10 +
    1.11 +typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
    1.12 +  unfolding sum_def by auto
    1.13  
    1.14  lemma Inl_RepI: "Inl_Rep a \<in> sum"
    1.15    by (auto simp add: sum_def)