# HG changeset patch # User berghofe # Date 835701534 -7200 # Node ID 88d4c33d794719406371aac9ffe989c01b2717ae # Parent 44254696843a28fd847502d8ebc838230cf55cf0 Changed argument order of nat_rec. 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)"