--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy Fri Feb 15 11:47:34 2013 +0100
@@ -0,0 +1,21 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate_Pretty_Char
+imports
+ Candidates
+ "~~/src/HOL/Library/AList_Mapping"
+ "~~/src/HOL/Library/Finite_Lattice"
+ "~~/src/HOL/Library/Code_Char"
+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