changeset 18551 | be0705186ff5 |
parent 16417 | 9bc16273c2d4 |
child 32960 | 69916a850301 |
--- a/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:16 2006 +0100 +++ b/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:55 2006 +0100 @@ -26,7 +26,7 @@ types mdecl = "mname \<times> methd" -record class +record "class" = super :: cname flds ::"fdecl list" methods ::"mdecl list" @@ -52,7 +52,7 @@ constdefs - class :: "cname \<rightharpoonup> class" + "class" :: "cname \<rightharpoonup> class" "class \<equiv> map_of Prog" is_class :: "cname => bool"