equal
deleted
inserted
replaced
153 where "the_Inl (Inl a) = a" |
153 where "the_Inl (Inl a) = a" |
154 |
154 |
155 primrec the_Inr :: "'a + 'b \<Rightarrow> 'b" |
155 primrec the_Inr :: "'a + 'b \<Rightarrow> 'b" |
156 where "the_Inr (Inr b) = b" |
156 where "the_Inr (Inr b) = b" |
157 |
157 |
158 datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c |
158 datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c |
159 |
159 |
160 primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a" |
160 primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a" |
161 where "the_In1 (In1 a) = a" |
161 where "the_In1 (In1 a) = a" |
162 |
162 |
163 primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b" |
163 primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b" |