| changeset 10835 | f4745d77e620 |
| parent 2380 | 90280b3a538b |
| child 12036 | 49f6c49454c2 |
| 10834:a7897aebbffc | 10835:f4745d77e620 |
|---|---|
30 p :: "'a -> 'a" |
30 p :: "'a -> 'a" |
31 q :: "'a -> 'a" |
31 q :: "'a -> 'a" |
32 |
32 |
33 defs |
33 defs |
34 |
34 |
35 p_def "p == fix`(LAM f. LAM x. |
35 p_def "p == fix$(LAM f. LAM x. |
36 If b1`x then f`(g`x) else x fi)" |
36 If b1$x then f$(g$x) else x fi)" |
37 |
37 |
38 q_def "q == fix`(LAM f. LAM x. |
38 q_def "q == fix$(LAM f. LAM x. |
39 If b1`x orelse b2`x then f`(g`x) else x fi)" |
39 If b1$x orelse b2$x then f$(g$x) else x fi)" |
40 |
40 |
41 end |
41 end |
42 |
42 |