changeset 124 | 858ab9a9b047 |
parent 0 | a5a9c433f639 |
123:0a2f744e008a | 124:858ab9a9b047 |
---|---|
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Least and greatest fixed points |
6 Least and greatest fixed points |
7 *) |
7 *) |
8 |
8 |
9 Fixedpt = ZF + |
9 Fixedpt = ZF + "domrange" + |
10 consts |
10 consts |
11 bnd_mono :: "[i,i=>i]=>o" |
11 bnd_mono :: "[i,i=>i]=>o" |
12 lfp, gfp :: "[i,i=>i]=>i" |
12 lfp, gfp :: "[i,i=>i]=>i" |
13 |
13 |
14 rules |
14 rules |