equal
deleted
inserted
replaced
4 section \<open>Pervasive test of code generator\<close> |
4 section \<open>Pervasive test of code generator\<close> |
5 |
5 |
6 theory Generate_Binary_Nat |
6 theory Generate_Binary_Nat |
7 imports |
7 imports |
8 Candidates |
8 Candidates |
9 "~~/src/HOL/Library/AList_Mapping" |
9 "HOL-Library.AList_Mapping" |
10 "~~/src/HOL/Library/Finite_Lattice" |
10 "HOL-Library.Finite_Lattice" |
11 "~~/src/HOL/Library/Code_Binary_Nat" |
11 "HOL-Library.Code_Binary_Nat" |
12 begin |
12 begin |
13 |
13 |
14 text \<open> |
14 text \<open> |
15 If any of the checks fails, inspect the code generated |
15 If any of the checks fails, inspect the code generated |
16 by a corresponding \<open>export_code\<close> command. |
16 by a corresponding \<open>export_code\<close> command. |