author | haftmann |
Sun, 13 Mar 2016 10:22:46 +0100 | |
changeset 62608 | 19f87fa0cfcb |
parent 58889 | 5b7a9633cfa8 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) section {* Pervasive test of code generator *} theory Generate_Binary_Nat imports Candidates "~~/src/HOL/Library/AList_Mapping" "~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Code_Binary_Nat" begin text {* If any of the checks fails, inspect the code generated by a corresponding @{text export_code} command. *} export_code _ checking SML OCaml? Haskell? Scala end