src/ZF/QUniv.thy
changeset 3923 c257b82a1200
parent 2469 b50b8c0eec01
child 3940 1d5bee4d047f
     1.1 --- a/src/ZF/QUniv.thy	Fri Oct 17 17:39:04 1997 +0200
     1.2 +++ b/src/ZF/QUniv.thy	Fri Oct 17 17:40:02 1997 +0200
     1.3 @@ -7,9 +7,14 @@
     1.4  *)
     1.5  
     1.6  QUniv = Univ + QPair + mono + equalities +
     1.7 +
     1.8 +global
     1.9 +
    1.10  consts
    1.11      quniv        :: i=>i
    1.12  
    1.13 +path QUniv
    1.14 +
    1.15  defs
    1.16      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    1.17