src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 58889 5b7a9633cfa8
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 section \<open>Pervasive test of code generator\<close>
     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 \<open>
    15   If any of the checks fails, inspect the code generated
    16   by a corresponding \<open>export_code\<close> command.
    17 \<close>
    18 
    19 export_code _ checking SML OCaml? Haskell? Scala
    20 
    21 end