isabelle: src/HOL/ex/Codegenerator_Pretty_Test.thy@04ce6bb14d85 (annotated)

31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	1
d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	3
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	4	header {* Pervasive test of code generator using pretty literals *}
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	5
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	6	theory Codegenerator_Pretty_Test
d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	7	imports Codegenerator_Pretty
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	8	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	9
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25933 diff changeset	10	export_code * in SML module_name CodegenTest
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25933 diff changeset	11	in OCaml module_name CodegenTest file -
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25933 diff changeset	12	in Haskell file -
25616 28d373f1482a added div/mod examples haftmann parents: 24530 diff changeset	13
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	14	end