src/ZF/Univ.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
--- a/src/ZF/Univ.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Univ.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,10 +13,10 @@
 
 Univ = Arith + Sum + Finite + "mono" +
 consts
-    Vfrom       :: "[i,i]=>i"
-    Vset        :: "i=>i"
-    Vrec        :: "[i, [i,i]=>i] =>i"
-    univ        :: "i=>i"
+    Vfrom       :: [i,i]=>i
+    Vset        :: i=>i
+    Vrec        :: [i, [i,i]=>i] =>i
+    univ        :: i=>i
 
 translations
     "Vset(x)"   == 	"Vfrom(0,x)"