equal
deleted
inserted
replaced
7 begin |
7 begin |
8 |
8 |
9 (**********************************************************************) |
9 (**********************************************************************) |
10 |
10 |
11 definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" |
11 definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" |
12 (infixr "\<box>" 55) |
12 (infixr \<open>\<box>\<close> 55) |
13 where |
13 where |
14 "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; |
14 "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; |
15 (xs2, x2) = f2 x1 |
15 (xs2, x2) = f2 x1 |
16 in (xs1 @ xs2, x2))" |
16 in (xs1 @ xs2, x2))" |
17 |
17 |