| changeset 11507 | 4b32a46ffd29 |
| parent 11499 | 7a7bb59a05db |
| child 11558 | 6539627881e8 |
| 11506:244a02a2968b | 11507:4b32a46ffd29 |
|---|---|
8 |
8 |
9 theory State = TypeRel: |
9 theory State = TypeRel: |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 body :: "imname => stmt" |
13 body :: "cname \<times> mname => stmt" |
14 "body \<equiv> \<lambda>(C,m). bdy (the (method C m))" |
14 "body \<equiv> \<lambda>(C,m). bdy (the (method C m))" |
15 |
15 |
16 text {* locations, i.e.\ abstract references to objects *} |
16 text {* locations, i.e.\ abstract references to objects *} |
17 typedecl loc |
17 typedecl loc |
18 |
18 |