src/HOL/Codegenerator_Test/Generate.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
     7 imports
     8   Candidates
     9   "~~/src/HOL/Library/AList_Mapping"
    10   "~~/src/HOL/Library/Finite_Lattice"
    11 begin
    12 
    13 text {*
    14   If any of the checks fails, inspect the code generated
    15   by a corresponding @{text export_code} command.
    16 *}
    17 
    18 export_code _ checking SML OCaml? Haskell? Scala
    19 
    20 end
    21