src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
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--
modernized header uniformly as section;
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 section {* 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