isabelle: src/HOL/ex/Codegenerator.thy@cc60e54aa7cb (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
21922 76e1fce071aa removed private files haftmann parents: 21911 diff changeset	11	code_gen "*" (SML #) (Haskell -) (OCaml -)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	12
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	13	end

author	chaieb
	Sat, 06 Jan 2007 20:47:09 +0100
changeset 22026	cc60e54aa7cb
parent 21922	76e1fce071aa
child 22297	757ace95c4a0
permissions	-rw-r--r--