src/HOL/Codegenerator_Test/Generate.thy
author Christian Sternagel
Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093 fdc301f592c4
parent 40711 81bc73585eec
child 50629 264ece81df93
permissions -rw-r--r--
forgot to add lemmas
haftmann@19281
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@19281
     3
haftmann@31378
     4
header {* Pervasive test of code generator *}
haftmann@19281
     5
haftmann@37695
     6
theory Generate
haftmann@37695
     7
imports Candidates
haftmann@31378
     8
begin
haftmann@24430
     9
haftmann@37745
    10
subsection {* Check whether generated code compiles *}
haftmann@37745
    11
haftmann@37745
    12
text {*
haftmann@37824
    13
  If any of the checks fails, inspect the code generated
haftmann@37824
    14
  by a corresponding @{text export_code} command.
haftmann@37745
    15
*}
haftmann@37745
    16
haftmann@40711
    17
export_code _ checking SML OCaml? Haskell? Scala?
haftmann@19281
    18
wenzelm@23266
    19
end