equal
deleted
inserted
replaced
7 header "Java Values" |
7 header "Java Values" |
8 |
8 |
9 theory Value = Type: |
9 theory Value = Type: |
10 |
10 |
11 typedecl loc (* locations, i.e. abstract references on objects *) |
11 typedecl loc (* locations, i.e. abstract references on objects *) |
12 arities loc :: "term" |
|
13 |
12 |
14 datatype val |
13 datatype val |
15 = Unit (* dummy result value of void methods *) |
14 = Unit (* dummy result value of void methods *) |
16 | Null (* null reference *) |
15 | Null (* null reference *) |
17 | Bool bool (* Boolean value *) |
16 | Bool bool (* Boolean value *) |