isabelle: src/HOL/ex/Codegenerator_Pretty.thy@1c93cfa807bc (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
7d1a16c77f7c tuned haftmann parents: diff changeset	6	theory Codegenerator_Pretty
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	7	imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	8	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	9
28562 4e74209f113e `code func` now just `code` haftmann parents: 28335 diff changeset	10	declare isnorm.simps [code del]
28228 7ebe8dc06cbb evaluation using code generator haftmann parents: 26468 diff changeset	11
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	12	end