src/ZF/QUniv.thy
author wenzelm
Tue Jan 12 15:17:37 1999 +0100 (1999-01-12 ago)
changeset 6093 87bf8c03b169
parent 3940 1d5bee4d047f
child 6112 5e4871c5136b
permissions -rw-r--r--
eliminated global/local names;
wenzelm@6093
     1
(*  Title:      ZF/QUniv.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
wenzelm@6093
     6
A small universe for lazy recursive types.
clasohm@0
     7
*)
clasohm@0
     8
paulson@2469
     9
QUniv = Univ + QPair + mono + equalities +
wenzelm@3923
    10
wenzelm@6093
    11
constdefs
wenzelm@6093
    12
  quniv :: i => i
wenzelm@6093
    13
  "quniv(A) == Pow(univ(eclose(A)))"
clasohm@0
    14
clasohm@0
    15
end