equal
deleted
inserted
replaced
7 header {* \isaheader{Program State} *} |
7 header {* \isaheader{Program State} *} |
8 |
8 |
9 theory State imports TypeRel Value begin |
9 theory State imports TypeRel Value begin |
10 |
10 |
11 types |
11 types |
12 fields_ = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value" |
12 fields' = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value" |
13 |
13 |
14 obj = "cname \<times> fields_" -- "class instance with class name and fields" |
14 obj = "cname \<times> fields'" -- "class instance with class name and fields" |
15 |
15 |
16 constdefs |
16 constdefs |
17 obj_ty :: "obj => ty" |
17 obj_ty :: "obj => ty" |
18 "obj_ty obj == Class (fst obj)" |
18 "obj_ty obj == Class (fst obj)" |
19 |
19 |