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/Types.thy
changeset 11318 6536fb8c9fc6
parent 6112 5e4871c5136b
child 12595 0480d02221b8 
--- a/src/ZF/Coind/Types.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Types.thy	Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
   TyConst :: i          (* Abstract type of type constants *)
 
 datatype
-  "Ty" = t_const ("tc:TyConst")
-       | t_fun ("t1:Ty","t2:Ty")
+  "Ty" = t_const ("tc \\<in> TyConst")
+       | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
   
 
 (* Definition of type environments and associated operators *)
@@ -22,7 +22,7 @@
 
 datatype
   "TyEnv" = te_emp
-          | te_owr ("te:TyEnv","x:ExVar","t:Ty") 
+          | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty") 
 
 consts
   te_dom :: i => i
isabelle