| changeset 36452 | d37c6eed8117 |
| parent 35932 | 86559356502d |
| 36451:ddc965e172c4 | 36452:d37c6eed8117 |
|---|---|
6 |
6 |
7 theory Letrec |
7 theory Letrec |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 defaultsort pcpo |
11 default_sort pcpo |
12 |
12 |
13 definition |
13 definition |
14 CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where |
14 CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where |
15 "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))" |
15 "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))" |
16 |
16 |