isabelle: src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy@a91e32843310 (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
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 62390 diff changeset	7	theory Compute_Oracle imports HOL.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
62390 842917225d56 more canonical names nipkow parents: 48891 diff changeset	19	end

author	wenzelm
	Thu, 03 Jan 2019 20:16:42 +0100
changeset 69584	a91e32843310
parent 66453	cc19f7ca2ed6
child 69605	a96320074298
permissions	-rw-r--r--