--- a/src/ZF/Coind/Language.thy Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Language.thy Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
c_app :: [i,i] => i (*Abstract constructor for fun application*)
rules
- constNEE "c:Const ==> c ~= 0"
- c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+ constNEE "c \\<in> Const ==> c \\<noteq> 0"
+ c_appI "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
consts
@@ -20,10 +20,10 @@
ExVar :: i (* Abstract type of variables *)
datatype
- "Exp" = e_const ("c:Const")
- | e_var ("x:ExVar")
- | e_fn ("x:ExVar","e:Exp")
- | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
- | e_app ("e1:Exp","e2:Exp")
+ "Exp" = e_const ("c \\<in> Const")
+ | e_var ("x \\<in> ExVar")
+ | e_fn ("x \\<in> ExVar","e \\<in> Exp")
+ | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
+ | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
end