isabelle: src/HOL/ex/Codegenerator.thy@5d63184c10c7 (annotated)

19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	1	(* ID: $Id$
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	3	*)
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	4
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	5	header {* Tests and examples for code generator *}
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	6
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	7	theory Codegenerator
21911 e29bcab0c81c added OCaml code generation (without dictionaries) haftmann parents: 21898 diff changeset	8	imports ExecutableContent
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	9	begin
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	10
24432 d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	11	ML {* (FIXME get rid of this)
24430 df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	12	nonfix union;
df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	13	nonfix inter;
24718 16b11ba36350 made SML/NJ happy haftmann parents: 24432 diff changeset	14	nonfix upto;
24430 df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	15	*}
df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	16
24423 ae9cd0e92423 overloaded definitions accompanied by explicit constants haftmann parents: 24348 diff changeset	17	export_code * in SML module_name CodegenTest
24810 862b71696efe ignore mutual recursive modules haftmann parents: 24718 diff changeset	18	in OCaml module_name CodegenTest file -
23811 b18557301bf9 added function for case certificates haftmann parents: 23266 diff changeset	19	in Haskell file -
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	20
24432 d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	21	ML {*
d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	22	infix union;
d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	23	infix inter;
24718 16b11ba36350 made SML/NJ happy haftmann parents: 24432 diff changeset	24	infix 4 upto;
24432 d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	25	*}
d555d941f983 circumvented infix problem haftmann parents: 24430 diff changeset	26
23266 50f0a4f12ed3 tuned document; wenzelm parents: 22845 diff changeset	27	end

author	haftmann
	Fri, 24 Oct 2008 17:48:39 +0200
changeset 28686	5d63184c10c7
parent 28335	25326092cf9a
permissions	-rw-r--r--