isabelle: src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy@6f9e24376ffd (annotated)

41959 b460124855b8 tuned headers; wenzelm parents: 37872 diff changeset	1	(* Title: HOL/Matrix/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
25217 3224db6415ae better compute oracle obua parents: 23663 diff changeset	8	uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
23173 51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	9	begin
51179ca0c429 proper theory setup for compute oracle (based on CPure); wenzelm parents: diff changeset	10
23663 84b5c89b8b49 new version of computing oracle obua parents: 23173 diff changeset	11	end