src/HOL/Bali/Decl.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 35547 991a6af75978
     1.1 --- a/src/HOL/Bali/Decl.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/Decl.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -149,24 +149,24 @@
     1.4          access :: acc_modi
     1.5  
     1.6  translations
     1.7 -  "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
     1.8 -  "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
     1.9 +  (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
    1.10 +  (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
    1.11  
    1.12  subsection {* Member (field or method)*}
    1.13  record  member = decl +
    1.14           static :: stat_modi
    1.15  
    1.16  translations
    1.17 -  "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
    1.18 -  "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
    1.19 +  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
    1.20 +  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
    1.21  
    1.22  subsection {* Field *}
    1.23  
    1.24  record field = member +
    1.25          type :: ty
    1.26  translations
    1.27 -  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
    1.28 -  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
    1.29 +  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
    1.30 +  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
    1.31  
    1.32  types     
    1.33          fdecl           (* field declaration, cf. 8.3 *)
    1.34 @@ -174,7 +174,7 @@
    1.35  
    1.36  
    1.37  translations
    1.38 -  "fdecl" <= (type) "vname \<times> field"
    1.39 +  (type) "fdecl" <= (type) "vname \<times> field"
    1.40  
    1.41  subsection  {* Method *}
    1.42  
    1.43 @@ -193,17 +193,17 @@
    1.44  
    1.45  
    1.46  translations
    1.47 -  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.48 +  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.49                        pars::vname list, resT::ty\<rparr>"
    1.50 -  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.51 +  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.52                        pars::vname list, resT::ty,\<dots>::'a\<rparr>"
    1.53 -  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
    1.54 -  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
    1.55 -  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.56 +  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
    1.57 +  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
    1.58 +  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.59                        pars::vname list, resT::ty,mbody::mbody\<rparr>"
    1.60 -  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.61 +  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
    1.62                        pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
    1.63 -  "mdecl" <= (type) "sig \<times> methd"
    1.64 +  (type) "mdecl" <= (type) "sig \<times> methd"
    1.65  
    1.66  
    1.67  definition mhead :: "methd \<Rightarrow> mhead" where
    1.68 @@ -306,13 +306,13 @@
    1.69          = "qtname \<times> iface"
    1.70  
    1.71  translations
    1.72 -  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
    1.73 -  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
    1.74 -  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    1.75 +  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
    1.76 +  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
    1.77 +  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    1.78                        isuperIfs::qtname list\<rparr>"
    1.79 -  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    1.80 +  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
    1.81                        isuperIfs::qtname list,\<dots>::'a\<rparr>"
    1.82 -  "idecl" <= (type) "qtname \<times> iface"
    1.83 +  (type) "idecl" <= (type) "qtname \<times> iface"
    1.84  
    1.85  definition ibody :: "iface \<Rightarrow> ibody" where
    1.86    "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
    1.87 @@ -337,17 +337,17 @@
    1.88          = "qtname \<times> class"
    1.89  
    1.90  translations
    1.91 -  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.92 +  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.93                        methods::mdecl list,init::stmt\<rparr>"
    1.94 -  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.95 +  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.96                        methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
    1.97 -  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.98 +  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
    1.99                        methods::mdecl list,init::stmt,
   1.100                        super::qtname,superIfs::qtname list\<rparr>"
   1.101 -  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
   1.102 +  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
   1.103                        methods::mdecl list,init::stmt,
   1.104                        super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
   1.105 -  "cdecl" <= (type) "qtname \<times> class"
   1.106 +  (type) "cdecl" <= (type) "qtname \<times> class"
   1.107  
   1.108  definition cbody :: "class \<Rightarrow> cbody" where
   1.109    "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
   1.110 @@ -404,8 +404,8 @@
   1.111          "classes"::"cdecl list"
   1.112  
   1.113  translations
   1.114 -     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
   1.115 -     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
   1.116 +     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
   1.117 +     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
   1.118  
   1.119  abbreviation
   1.120    iface :: "prog  \<Rightarrow> (qtname, iface) table"