equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Type of indices *} |
3 header {* Type of indices *} |
4 |
4 |
5 theory Code_Index |
5 theory Code_Index |
6 imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 text {* |
9 text {* |
10 Indices are isomorphic to HOL @{typ nat} but |
10 Indices are isomorphic to HOL @{typ nat} but |
11 mapped to target-language builtin integers. |
11 mapped to target-language builtin integers. |