changeset 124 | 858ab9a9b047 |
parent 0 | a5a9c433f639 |
child 753 | ec86863e87c8 |
123:0a2f744e008a | 124:858ab9a9b047 |
---|---|
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 A small universe for lazy recursive types |
6 A small universe for lazy recursive types |
7 *) |
7 *) |
8 |
8 |
9 QUniv = Univ + QPair + |
9 QUniv = Univ + QPair + "mono" + "equalities" + |
10 consts |
10 consts |
11 quniv :: "i=>i" |
11 quniv :: "i=>i" |
12 |
12 |
13 rules |
13 rules |
14 quniv_def "quniv(A) == Pow(univ(eclose(A)))" |
14 quniv_def "quniv(A) == Pow(univ(eclose(A)))" |