isabelle: src/HOL/Codegenerator_Test/Candidates_Pretty.thy@fc48faccd77b (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
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 31378 diff changeset	7	imports Candidates Code_Char 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