--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/QUniv.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,16 @@
+(*  Title: 	ZF/univ.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+A small universe for lazy recursive types
+*)
+
+QUniv = Univ + QPair +
+consts
+    quniv        :: "i=>i"
+
+rules
+    quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
+
+end