--- a/src/HOL/MicroJava/J/Decl.thy Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Dec 06 19:10:36 2000 +0100
@@ -19,7 +19,7 @@
= "sig \\<times> ty \\<times> 'c"
types 'c class (* class *)
- = "cname option \\<times> fdecl list \\<times> 'c mdecl list"
+ = "cname \\<times> fdecl list \\<times> 'c mdecl list"
(* superclass, fields, methods*)
'c cdecl (* class declaration, cf. 8.1 *)
@@ -32,23 +32,33 @@
defs
- ObjectC_def "ObjectC == (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
types 'c prog = "'c cdecl list"
+
+translations
+ "fdecl" <= (type) "vname \\<times> ty"
+ "sig" <= (type) "mname \\<times> ty list"
+ "mdecl c" <= (type) "sig \\<times> ty \\<times> c"
+ "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list"
+ "cdecl c" <= (type) "cname \\<times> (c class)"
+ "prog c" <= (type) "(c cdecl) list"
+
consts
class :: "'c prog => (cname \\<leadsto> 'c class)"
+ is_class :: "'c prog => cname => bool"
- is_class :: "'c prog => cname => bool"
- is_type :: "'c prog => ty => bool"
+translations
-defs
+ "class" => "map_of"
+ "is_class G C" == "class G C \\<noteq> None"
- class_def "class == map_of"
+consts
- is_class_def "is_class G C == class G C \\<noteq> None"
+ is_type :: "'c prog => ty => bool"
primrec
"is_type G (PrimT pt) = True"