equal
deleted
inserted
replaced
12 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
12 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
13 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
13 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
14 |
14 |
15 defs |
15 defs |
16 |
16 |
17 step_def "step == (LAM b g x. If b`x then g`x else x fi)" |
17 step_def "step == (LAM b g x. If b$x then g$x else x fi)" |
18 while_def "while == (LAM b g. fix`(LAM f x. |
18 while_def "while == (LAM b g. fix$(LAM f x. |
19 If b`x then f`(g`x) else x fi))" |
19 If b$x then f$(g$x) else x fi))" |
20 |
20 |
21 end |
21 end |
22 |
22 |