src/ZF/Univ.thy

--- a/src/ZF/Univ.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Univ.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -17,9 +17,9 @@
   Vfrom       :: "[i,i]=>i"
     "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
 
-syntax   Vset :: "i=>i"
-translations
-    "Vset(x)"   ==      "Vfrom(0,x)"
+abbreviation
+  Vset :: "i=>i" where
+  "Vset(x) == Vfrom(0,x)"
 
 
 constdefs