isabelle: src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy@557302525778 (annotated)

47455 26315a545e26 updated headers; wenzelm parents: 46988 diff changeset	1	(* Title: HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	2	Author: Steven Obua, TU Munich
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	3
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	4	Steven Obua's evaluator.
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	5	*)
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	6
37869 e9c6a7fe1989 explicit dependency on theory HOL; wenzelm parents: 30161 diff changeset	7	theory Compute_Oracle imports HOL
23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	8	begin
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	9
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	10	ML_file "am.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	11	ML_file "am_compiler.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	12	ML_file "am_interpreter.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	13	ML_file "am_ghc.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	14	ML_file "am_sml.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	15	ML_file "report.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	16	ML_file "compute.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	17	ML_file "linker.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	18
23663 84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	19	end

author	blanchet
	Wed, 26 Sep 2012 10:00:59 +0200
changeset 49582	557302525778
parent 48891	c0eafbd55de3
child 62390	842917225d56
permissions	-rw-r--r--