isabelle: src/HOL/ex/Codegenerator.thy@c3654ba76a09 (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
	Fri, 16 Mar 2007 21:32:10 +0100
changeset 22454	c3654ba76a09
parent 22297	757ace95c4a0
child 22845	5f9138bcb3d7
permissions	-rw-r--r--