isabelle: src/HOL/Codegenerator_Test/Candidates_Pretty.thy@6ef538f6a8ab (annotated)

24195 7d1a16c77f7c tuned haftmann parents: diff changeset	1
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	3
d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	4	header {* Generating code using pretty literals and natural number literals *}
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 31378 diff changeset	6	theory Candidates_Pretty
42842 6ef538f6a8ab adding Code_Char_ord to code generation regression tests bulwahn parents: 37695 diff changeset	7	imports Candidates Code_Char_ord Efficient_Nat
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	8	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	9
7d1a16c77f7c tuned haftmann parents: diff changeset	10	end