isabelle: src/HOL/ex/Codegenerator.thy@3e29eafabe16 (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
24348 c708ea5b109a renamed code_gen to export_code haftmann parents: 24249 diff changeset	11	export_code "*" in SML module_name CodegenTest
23811 b18557301bf9 added function for case certificates haftmann parents: 23266 diff changeset	12	in OCaml file -
b18557301bf9 added function for case certificates haftmann parents: 23266 diff changeset	13	in Haskell 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	huffman
	Mon, 20 Aug 2007 23:00:17 +0200
changeset 24367	3e29eafabe16
parent 24348	c708ea5b109a
child 24423	ae9cd0e92423
permissions	-rw-r--r--