isabelle: src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy@4b620e1cb1e9 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	10	ML_file \<open>am.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	11	ML_file \<open>am_compiler.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	12	ML_file \<open>am_interpreter.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	13	ML_file \<open>am_ghc.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	14	ML_file \<open>am_sml.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	15	ML_file \<open>report.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	16	ML_file \<open>compute.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	17	ML_file \<open>linker.ML\<close>
48891 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
	Tue, 05 Jan 2021 17:40:51 +0100
changeset 73060	4b620e1cb1e9
parent 69605	a96320074298
permissions	-rw-r--r--