src/HOL/Codegenerator_Test/Generate.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
haftmann@19281
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@19281
     3
wenzelm@58889
     4
section {* Pervasive test of code generator *}
haftmann@19281
     5
haftmann@37695
     6
theory Generate
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@31378
    11
begin
haftmann@24430
    12
haftmann@37745
    13
text {*
haftmann@37824
    14
  If any of the checks fails, inspect the code generated
haftmann@37824
    15
  by a corresponding @{text export_code} command.
haftmann@37745
    16
*}
haftmann@37745
    17
haftmann@50629
    18
export_code _ checking SML OCaml? Haskell? Scala
haftmann@19281
    19
wenzelm@23266
    20
end
haftmann@51161
    21