author | nipkow |
Mon, 06 Aug 2001 13:43:24 +0200 | |
changeset 11464 | ddea204de5bc |
parent 124 | 858ab9a9b047 |
permissions | -rw-r--r-- |
(* 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 + "mono" + "equalities" + consts quniv :: "i=>i" rules quniv_def "quniv(A) == Pow(univ(eclose(A)))" end