changeset 1558 | 9c6ebfab4e05 |
parent 1475 | 7f5a4cd08209 |
child 3947 | eb707467f8c5 |
1557:fe30812f5b5e | 1558:9c6ebfab4e05 |
---|---|
5 |
5 |
6 Greatest fixed points (requires Lfp too!) |
6 Greatest fixed points (requires Lfp too!) |
7 *) |
7 *) |
8 |
8 |
9 Gfp = Lfp + |
9 Gfp = Lfp + |
10 consts gfp :: ['a set=>'a set] => 'a set |
10 |
11 defs |
11 constdefs |
12 (*greatest fixed point*) |
12 gfp :: ['a set=>'a set] => 'a set |
13 gfp_def "gfp(f) == Union({u. u <= f(u)})" |
13 "gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*) |
14 |
|
14 end |
15 end |