| changeset 68451 | c34aa23a1fb6 |
| parent 67443 | 3abf6a722518 |
| child 69597 | ff784d5a5bfb |
--- a/src/HOL/NanoJava/State.thy Fri Jun 15 10:45:12 2018 +0200 +++ b/src/HOL/NanoJava/State.thy Fri Jun 15 13:02:12 2018 +0200 @@ -45,7 +45,7 @@ (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)" definition del_locs :: "state => state" where - "del_locs s \<equiv> s (| locals := empty |)" + "del_locs s \<equiv> s (| locals := Map.empty |)" definition init_locs :: "cname => mname => state => state" where "init_locs C m s \<equiv> s (| locals := locals s ++