isabelle: src/HOL/ex/Codegenerator.thy@7b52c4fde622 (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
22845 5f9138bcb3d7 changed code generator invocation syntax haftmann parents: 22297 diff changeset	11	code_gen "*" in SML in OCaml file - in OCaml file -
5f9138bcb3d7 changed code generator invocation syntax haftmann parents: 22297 diff changeset	12	code_gen in SML in OCaml file - in OCaml file -
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
	Sat, 19 May 2007 11:33:28 +0200
changeset 23023	7b52c4fde622
parent 22845	5f9138bcb3d7
child 23266	50f0a4f12ed3
permissions	-rw-r--r--