--- a/src/HOL/MicroJava/J/Decl.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Sep 21 10:42:49 2000 +0200
@@ -32,26 +32,26 @@
defs
- ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (None, [], []))"
types 'c prog = "'c cdecl list"
consts
- class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
+ class :: "'c prog => (cname \\<leadsto> 'c class)"
- is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
- is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
+ is_class :: "'c prog => cname => bool"
+ is_type :: "'c prog => ty => bool"
defs
- class_def "class \\<equiv> map_of"
+ class_def "class == map_of"
- is_class_def "is_class G C \\<equiv> class G C \\<noteq> None"
+ is_class_def "is_class G C == class G C \\<noteq> None"
primrec
"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
+"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
end