equal
deleted
inserted
replaced
6 |
6 |
7 header {* \isaheader{Java Values} *} |
7 header {* \isaheader{Java Values} *} |
8 |
8 |
9 theory Value imports Type begin |
9 theory Value imports Type begin |
10 |
10 |
11 typedecl loc_ -- "locations, i.e. abstract references on objects" |
11 typedecl loc' -- "locations, i.e. abstract references on objects" |
12 |
12 |
13 datatype loc |
13 datatype loc |
14 = XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
14 = XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
15 | Loc loc_ -- "usual locations (references on objects)" |
15 | Loc loc' -- "usual locations (references on objects)" |
16 |
16 |
17 datatype val |
17 datatype val |
18 = Unit -- "dummy result value of void methods" |
18 = Unit -- "dummy result value of void methods" |
19 | Null -- "null reference" |
19 | Null -- "null reference" |
20 | Bool bool -- "Boolean value" |
20 | Bool bool -- "Boolean value" |