author | berghofe |
Tue, 25 Jun 1996 13:18:54 +0200 | |
changeset 1825 | 88d4c33d7947 |
parent 1824 | 44254696843a |
child 1826 | 2a2c0dbeb4ac |
src/HOLCF/Fix.thy | file | annotate | diff | comparison | revisions |
--- 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)"