src/ZF/QUniv.thy

+(*  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