equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Type of target language numerals *} |
3 header {* Type of target language numerals *} |
4 |
4 |
5 theory Code_Numeral |
5 theory Code_Numeral |
6 imports Nat_Numeral Divides |
6 imports Nat_Numeral Nat_Transfer Divides |
7 begin |
7 begin |
8 |
8 |
9 text {* |
9 text {* |
10 Code numerals are isomorphic to HOL @{typ nat} but |
10 Code numerals are isomorphic to HOL @{typ nat} but |
11 mapped to target-language builtin numerals. |
11 mapped to target-language builtin numerals. |