equal
deleted
inserted
replaced
31 "obj" \<leftharpoondown> (type)"cname \<times> fields" |
31 "obj" \<leftharpoondown> (type)"cname \<times> fields" |
32 |
32 |
33 constdefs |
33 constdefs |
34 |
34 |
35 init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" |
35 init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" |
36 "init_vars m == option_map (\<lambda>T. Null) o m" |
36 "init_vars m == Option.map (\<lambda>T. Null) o m" |
37 |
37 |
38 text {* private: *} |
38 text {* private: *} |
39 types heap = "loc \<rightharpoonup> obj" |
39 types heap = "loc \<rightharpoonup> obj" |
40 locals = "vname \<rightharpoonup> val" |
40 locals = "vname \<rightharpoonup> val" |
41 |
41 |