author | paulson |
Thu, 07 Jan 1999 10:56:05 +0100 | |
changeset 6068 | 2d8f3e1f1151 |
parent 3940 | 1d5bee4d047f |
child 6093 | 87bf8c03b169 |
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 + global consts quniv :: i=>i local defs quniv_def "quniv(A) == Pow(univ(eclose(A)))" end