Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/Decl.thy
changeset 18551 be0705186ff5
parent 16417 9bc16273c2d4
child 35416 d8d7d1b785af 
--- a/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:55 2006 +0100
@@ -15,7 +15,7 @@
 
   'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
 
-  'c class = "cname \<times> fdecl list \<times> 'c mdecl list" 
+  'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
   -- "class = superclass, fields, methods"
 
   'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
@@ -33,7 +33,7 @@
 
 
 constdefs
-  class :: "'c prog => (cname \<rightharpoonup> 'c class)"
+  "class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
   "class \<equiv> map_of"
 
   is_class :: "'c prog => cname => bool"
isabelle