diff -r 44254696843a -r 88d4c33d7947 src/HOLCF/Fix.thy --- 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)"