author | wenzelm |
Thu, 26 May 2016 17:51:22 +0200 | |
changeset 63167 | 0909deb8059b |
parent 58889 | 5b7a9633cfa8 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) section \<open>Pervasive test of code generator\<close> theory Generate_Target_Nat imports Candidates "~~/src/HOL/Library/AList_Mapping" "~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Code_Target_Numeral" begin text \<open> If any of the checks fails, inspect the code generated by a corresponding \<open>export_code\<close> command. \<close> export_code _ checking SML OCaml? Haskell? Scala end