changeset 14134 | 0fdf5708c7a8 |
parent 14045 | a34d89ce6097 |
child 16417 | 9bc16273c2d4 |
--- a/src/HOL/MicroJava/J/WellType.thy Fri Jul 25 10:52:15 2003 +0200 +++ b/src/HOL/MicroJava/J/WellType.thy Fri Jul 25 17:21:22 2003 +0200 @@ -24,12 +24,12 @@ text "local variables, including method parameters and This:" types - lenv = "vname \<leadsto> ty" + lenv = "vname \<rightharpoonup> ty" 'c env = "'c prog \<times> lenv" syntax prg :: "'c env => 'c prog" - localT :: "'c env => (vname \<leadsto> ty)" + localT :: "'c env => (vname \<rightharpoonup> ty)" translations "prg" => "fst"