isabelle: src/HOL/Codegenerator_Test/Generate.thy@71e84a203c19 (annotated)

19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	1
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	3
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	4	header {* Pervasive test of code generator *}
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	6	theory Generate
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	7	imports Candidates
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	8	begin
24430 df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	9
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	10	export_code * in SML module_name Code_Test
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	11	in OCaml module_name Code_Test file -
23811 b18557301bf9 added function for case certificates haftmann parents: 23266 diff changeset	12	in Haskell file -
34306 e8b8ee60c1e2 simple tests haftmann parents: 31378 diff changeset	13	in Scala file -
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	14
23266 50f0a4f12ed3 tuned document; wenzelm parents: 22845 diff changeset	15	end

author	haftmann
	Fri, 02 Jul 2010 14:23:18 +0200
changeset 37695	71e84a203c19
parent 34306	src/HOL/ex/Codegenerator_Test.thy@e8b8ee60c1e2
child 37745	6315b6426200
permissions	-rw-r--r--