Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Coind/Values.thy
changeset 11318 6536fb8c9fc6
parent 6117 f9aad8ccd590
child 12595 0480d02221b8 
--- 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
isabelle