src/HOL/MicroJava/J/TypeRel.thy
changeset 14134 0fdf5708c7a8
parent 14045 a34d89ce6097
child 14171 0cab06e3bbd0
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 25 10:52:15 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 25 17:21:22 2003 +0200
     1.3 @@ -81,8 +81,8 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  method :: "'c prog \<times> cname => ( sig   \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
     1.8 -  field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
     1.9 +  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
    1.10 +  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    1.11    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    1.12  
    1.13  -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"