author | wenzelm |
Tue, 24 Nov 1998 12:03:09 +0100 | |
changeset 5953 | d6017ce6b93e |
parent 3940 | 1d5bee4d047f |
child 6093 | 87bf8c03b169 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/univ.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
A small universe for lazy recursive types |
|
7 |
*) |
|
8 |
||
2469 | 9 |
QUniv = Univ + QPair + mono + equalities + |
3923 | 10 |
|
11 |
global |
|
12 |
||
0 | 13 |
consts |
1401 | 14 |
quniv :: i=>i |
0 | 15 |
|
3940 | 16 |
local |
3923 | 17 |
|
753 | 18 |
defs |
0 | 19 |
quniv_def "quniv(A) == Pow(univ(eclose(A)))" |
20 |
||
21 |
end |