| changeset 1150 | 66512c9e6bd6 |
| parent 243 | c22b85994e17 |
| child 1168 | 74be52691d62 |
--- a/src/HOLCF/Dnat2.thy Wed Jun 21 15:01:07 1995 +0200 +++ b/src/HOLCF/Dnat2.thy Wed Jun 21 15:14:58 1995 +0200 @@ -16,8 +16,8 @@ rules -iterator_def "iterator = fix[LAM h n f x.\ -\ dnat_when[x][LAM m.f[h[m][f][x]]][n]]" +iterator_def "iterator = fix[LAM h n f x. + dnat_when[x][LAM m.f[h[m][f][x]]][n]]" end