--- a/src/ZF/univ.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/univ.thy Tue Nov 16 14:24:21 1993 +0100
@@ -8,7 +8,7 @@
Standard notation for Vset(i) is V(i), but users might want V for a variable
*)
-Univ = Arith + Sum +
+Univ = Arith + Sum + "mono" +
consts
Limit :: "i=>o"
Vfrom :: "[i,i]=>i"