--- a/src/ZF/Coind/Language.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Language.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,17 @@
Copyright 1995 University of Cambridge
*)
-Language = Main +
+theory Language = Main:
consts
Const :: i (* Abstract type of constants *)
- c_app :: [i,i] => i (* Abstract constructor for fun application*)
+ c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
+
-rules
- constNEE "c \\<in> Const ==> c \\<noteq> 0"
- c_appI "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
+text{*these really can't be definitions without losing the abstraction*}
+axioms
+ constNEE: "c \<in> Const ==> c \<noteq> 0"
+ c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
consts
@@ -20,10 +22,10 @@
ExVar :: i (* Abstract type of variables *)
datatype
- "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")
+ "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