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
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* Pervasive test of code generator *}
     5 
     6 theory Generate
     7 imports Candidates
     8 begin
     9 
    10 subsection {* Check whether generated code compiles *}
    11 
    12 text {*
    13   If any of the checks fails, inspect the code generated
    14   by a corresponding @{text export_code} command.
    15 *}
    16 
    17 export_code _ checking SML OCaml? Haskell? Scala?
    18 
    19 end