diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Values.thy	Mon May 21 14:46:30 2001 +0200
@@ -12,10 +12,10 @@
   Val, ValEnv, Val_ValEnv  :: i
 
 codatatype
-    "Val" = v_const ("c:Const")
-          | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
+    "Val" = v_const ("c \\<in> Const")
+          | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
   and
-    "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
+    "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
   monos       map_mono
   type_intrs  A_into_univ, mapQU