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 |
6 theory Generate |
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 begin |
11 begin |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 If any of the checks fails, inspect the code generated |
14 If any of the checks fails, inspect the code generated |
15 by a corresponding \<open>export_code\<close> command. |
15 by a corresponding \<open>export_code\<close> command. |