changeset 27487 | c8a6ce181805 |
parent 27368 | 9f90ac19e32b |
child 28042 | 1471f2974eb1 |
27486:c61507a98bff | 27487:c8a6ce181805 |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Type of indices *} |
5 header {* Type of indices *} |
6 |
6 |
7 theory Code_Index |
7 theory Code_Index |
8 imports Plain Presburger |
8 imports Plain "~~/src/HOL/Presburger" |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 Indices are isomorphic to HOL @{typ nat} but |
12 Indices are isomorphic to HOL @{typ nat} but |
13 mapped to target-language builtin integers. |
13 mapped to target-language builtin integers. |