src/ZF/QUniv.thy

--- a/src/ZF/QUniv.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QUniv.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -10,7 +10,7 @@
 consts
     quniv        :: "i=>i"
 
-rules
+defs
     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
 
 end