equal
deleted
inserted
replaced
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 section \<open>Pervasive test of code generator\<close> |
|
5 |
|
6 theory Generate_Pretty_Char |
|
7 imports |
|
8 Candidates |
|
9 "HOL-Library.AList_Mapping" |
|
10 "HOL-Library.Finite_Lattice" |
|
11 "HOL-Library.Code_Char" |
|
12 begin |
|
13 |
|
14 text \<open> |
|
15 If any of the checks fails, inspect the code generated |
|
16 by a corresponding \<open>export_code\<close> command. |
|
17 \<close> |
|
18 |
|
19 export_code _ checking SML OCaml? Haskell? Scala |
|
20 |
|
21 end |
|