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;
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@24195
     3
wenzelm@58889
     4
section {* Pervasive test of code generator *}
haftmann@24195
     5
haftmann@51161
     6
theory Generate_Pretty_Char
haftmann@51161
     7
imports
haftmann@51161
     8
  Candidates
haftmann@51161
     9
  "~~/src/HOL/Library/AList_Mapping"
haftmann@51161
    10
  "~~/src/HOL/Library/Finite_Lattice"
haftmann@51161
    11
  "~~/src/HOL/Library/Code_Char"
haftmann@24195
    12
begin
haftmann@24195
    13
haftmann@37745
    14
text {*
haftmann@37824
    15
  If any of the checks fails, inspect the code generated
haftmann@37824
    16
  by a corresponding @{text export_code} command.
haftmann@37745
    17
*}
haftmann@37745
    18
haftmann@50629
    19
export_code _ checking SML OCaml? Haskell? Scala
haftmann@25616
    20
haftmann@24195
    21
end