equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 Extend the state space by one element indicating a type error (or |
12 Extend the state space by one element indicating a type error (or |
13 other abnormal termination) *} |
13 other abnormal termination) *} |
14 datatype 'a type_error = TypeError | Normal 'a |
14 datatype_new 'a type_error = TypeError | Normal 'a |
15 |
15 |
16 |
16 |
17 abbreviation |
17 abbreviation |
18 fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e" |
18 fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e" |
19 where "fifth x == fst(snd(snd(snd(snd x))))" |
19 where "fifth x == fst(snd(snd(snd(snd x))))" |