author | wenzelm |
Wed, 15 Oct 1997 15:12:59 +0200 | |
changeset 3872 | a5839ecee7b8 |
parent 2469 | b50b8c0eec01 |
child 3923 | c257b82a1200 |
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 + |
0 | 10 |
consts |
1401 | 11 |
quniv :: i=>i |
0 | 12 |
|
753 | 13 |
defs |
0 | 14 |
quniv_def "quniv(A) == Pow(univ(eclose(A)))" |
15 |
||
16 |
end |