| changeset 1370 | 7361ac9b024d |
| parent 923 | ff1574a81019 |
| child 1475 | 7f5a4cd08209 |
| 1369:b82815e61b30 | 1370:7361ac9b024d |
|---|---|
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 consts gfp :: ['a set=>'a set] => 'a set |
11 defs |
11 defs |
12 (*greatest fixed point*) |
12 (*greatest fixed point*) |
13 gfp_def "gfp(f) == Union({u. u <= f(u)})" |
13 gfp_def "gfp(f) == Union({u. u <= f(u)})" |
14 end |
14 end |