isabelle: src/HOL/Codegenerator_Test/Generate_Pretty.thy@6607ccf77946 (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
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	6	theory Generate_Pretty
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	7	imports Candidates_Pretty
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	8	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	9
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	10	lemma [code, code del]: "nat_of_char = nat_of_char" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	11	lemma [code, code del]: "char_of_nat = char_of_nat" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	12	lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	13	lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	14
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	15	export_code * in SML module_name Code_Test
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	16	in OCaml module_name Code_Test file -
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25933 diff changeset	17	in Haskell file -
37475 98c6f9dc58d0 activated Scala code generator test haftmann parents: 34887 diff changeset	18	in Scala file -
25616 28d373f1482a added div/mod examples haftmann parents: 24530 diff changeset	19
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	20	end

author	haftmann
	Tue, 06 Jul 2010 09:21:13 +0200
changeset 37724	6607ccf77946
parent 37695	71e84a203c19
child 37745	6315b6426200
permissions	-rw-r--r--