| changeset 1825 | 88d4c33d7947 |
| parent 1479 | 21eb5e156d91 |
| child 1990 | 9e23119c0219 |
--- a/src/HOLCF/Fix.thy Tue Jun 25 13:11:29 1996 +0200 +++ b/src/HOLCF/Fix.thy Tue Jun 25 13:18:54 1996 +0200 @@ -22,7 +22,7 @@ defs -iterate_def "iterate n F c == nat_rec n c (%n x.F`x)" +iterate_def "iterate n F c == nat_rec c (%n x.F`x) n" Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" fix_def "fix == (LAM f. Ifix f)"