author | wenzelm |
Fri, 25 Apr 1997 15:08:25 +0200 | |
changeset 3053 | db72904b42fb |
parent 2469 | b50b8c0eec01 |
child 3923 | c257b82a1200 |
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