isabelle: src/HOL/ex/Codegenerator.thy@753123c89d72 (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
22297 757ace95c4a0 splut up code generation in two parts haftmann parents: 21922 diff changeset	11	code_gen "*" (SML) (Haskell) (OCaml)
757ace95c4a0 splut up code generation in two parts haftmann parents: 21922 diff changeset	12	code_gen (SML #) (Haskell -) (OCaml -)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	13
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	14	end

author	haftmann
	Tue, 20 Mar 2007 08:27:15 +0100
changeset 22473	753123c89d72
parent 22297	757ace95c4a0
child 22845	5f9138bcb3d7
permissions	-rw-r--r--