| author | wenzelm |
| Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) | |
| changeset 58889 | 5b7a9633cfa8 |
| parent 51161 | 6ed12ae3b3e1 |
| child 63167 | 0909deb8059b |
| permissions | -rw-r--r-- |
2 (* Author: Florian Haftmann, TU Muenchen *)
4 section {* Pervasive test of code generator *}
6 theory Generate_Target_Nat
7 imports
8 Candidates
9 "~~/src/HOL/Library/AList_Mapping"
10 "~~/src/HOL/Library/Finite_Lattice"
11 "~~/src/HOL/Library/Code_Target_Numeral"
12 begin
14 text {*
15 If any of the checks fails, inspect the code generated
16 by a corresponding @{text export_code} command.
17 *}
19 export_code _ checking SML OCaml? Haskell? Scala
21 end