src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
author haftmann
Fri Feb 15 11:47:34 2013 +0100 (2013-02-15)
changeset 51161 6ed12ae3b3e1
parent 51143 src/HOL/Codegenerator_Test/Generate_Pretty.thy@0a2371e7ced3
child 58889 5b7a9633cfa8
permissions -rw-r--r--
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* Pervasive test of code generator *}
     5 
     6 theory Generate_Pretty_Char
     7 imports
     8   Candidates
     9   "~~/src/HOL/Library/AList_Mapping"
    10   "~~/src/HOL/Library/Finite_Lattice"
    11   "~~/src/HOL/Library/Code_Char"
    12 begin
    13 
    14 text {*
    15   If any of the checks fails, inspect the code generated
    16   by a corresponding @{text export_code} command.
    17 *}
    18 
    19 export_code _ checking SML OCaml? Haskell? Scala
    20 
    21 end