isabelle: src/Tools/Compute_Oracle/Compute_Oracle.thy@ccd9cb15c062 (annotated)

23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	1	(* Title: Tools/Compute_Oracle/Compute_Oracle.thy
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	2	ID: $Id$
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	3	Author: Steven Obua, TU Munich
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	4
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	5	Steven Obua's evaluator.
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	6	*)
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	7
23663 84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	8	theory Compute_Oracle imports CPure
84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	9	uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML"
23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	10	begin
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	11
23663 84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	12	setup {* Compute.setup; *}
23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	13
23663 84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	14	end

author	wenzelm
	Tue, 10 Jul 2007 23:29:43 +0200
changeset 23719	ccd9cb15c062
parent 23663	84b5c89b8b49
child 25217	3224db6415ae
permissions	-rw-r--r--