equal
deleted
inserted
replaced
6 |
6 |
7 theory Value imports Type begin |
7 theory Value imports Type begin |
8 |
8 |
9 typedecl loc' -- "locations, i.e. abstract references on objects" |
9 typedecl loc' -- "locations, i.e. abstract references on objects" |
10 |
10 |
11 datatype_new loc |
11 datatype loc |
12 = XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
12 = XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
13 | Loc loc' -- "usual locations (references on objects)" |
13 | Loc loc' -- "usual locations (references on objects)" |
14 |
14 |
15 datatype_new val |
15 datatype val |
16 = Unit -- "dummy result value of void methods" |
16 = Unit -- "dummy result value of void methods" |
17 | Null -- "null reference" |
17 | Null -- "null reference" |
18 | Bool bool -- "Boolean value" |
18 | Bool bool -- "Boolean value" |
19 | Intg int -- "integer value, name Intg instead of Int because |
19 | Intg int -- "integer value, name Intg instead of Int because |
20 of clash with HOL/Set.thy" |
20 of clash with HOL/Set.thy" |