| changeset 21404 | eb85850d3eb7 |
| parent 19764 | 372065f34795 |
| child 27108 | e447b3107696 |
--- a/src/HOLCF/ex/Dnat.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOLCF/ex/Dnat.thy Fri Nov 17 02:20:03 2006 +0100 @@ -10,7 +10,7 @@ domain dnat = dzero | dsucc (dpred :: dnat) definition - iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" + iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where "iterator = fix $ (LAM h n f x. case n of dzero => x | dsucc $ m => f $ (h $ m $ f $ x))"