author | lcp |
Thu, 12 Jan 1995 03:01:40 +0100 | |
changeset 852 | 664052e3cf66 |
parent 753 | ec86863e87c8 |
child 1401 | 0c439768f45c |
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" defs quniv_def "quniv(A) == Pow(univ(eclose(A)))" end