src/ZF/QUniv.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 1401 0c439768f45c
--- 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