equal
deleted
inserted
replaced
3 section \<open>Test of target-language bit operations\<close> |
3 section \<open>Test of target-language bit operations\<close> |
4 |
4 |
5 theory Generate_Target_Bit_Operations |
5 theory Generate_Target_Bit_Operations |
6 imports |
6 imports |
7 "HOL-Library.Code_Test" |
7 "HOL-Library.Code_Test" |
8 "HOL-Library.Code_Target_Bit_Shifts" |
|
9 begin |
8 begin |
10 |
9 |
11 context |
10 context |
12 includes bit_operations_syntax |
11 includes bit_operations_syntax |
13 begin |
12 begin |
62 |
61 |
63 text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close> |
62 text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close> |
64 |
63 |
65 qualified definition \<open>check_max = ()\<close> |
64 qualified definition \<open>check_max = ()\<close> |
66 |
65 |
67 qualified definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close> |
66 qualified definition \<open>anchor = (Code_Numeral.drop_bit, check_max)\<close> |
68 |
67 |
69 end |
68 end |
70 |
69 |
71 code_printing |
70 code_printing |
72 code_module Check_Max \<rightharpoonup> |
71 code_module Check_Max \<rightharpoonup> |