| author | nipkow |
| Thu, 11 Jul 2013 21:34:37 +0200 | |
| changeset 52593 | aedf7b01c6e4 |
| parent 51161 | 6ed12ae3b3e1 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) header {* Pervasive test of code generator *} theory Generate_Pretty_Char imports Candidates "~~/src/HOL/Library/AList_Mapping" "~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Code_Char" begin text {* If any of the checks fails, inspect the code generated by a corresponding @{text export_code} command. *} export_code _ checking SML OCaml? Haskell? Scala end