src/HOL/NanoJava/Decl.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 42463 f270e3e18be5
--- a/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -38,11 +38,11 @@
         = "cdecl list"
 
 translations
-  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
-  "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
-  "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
-  "cdecl" \<leftharpoondown> (type)"cname \<times> class"
-  "prog " \<leftharpoondown> (type)"cdecl list"
+  (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
+  (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
+  (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
+  (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
+  (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
 consts