author | wenzelm |
Sun, 06 Jan 2019 15:04:34 +0100 | |
changeset 69605 | a96320074298 |
parent 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
47455 | 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 | 10 |
ML_file \<open>am.ML\<close> |
11 |
ML_file \<open>am_compiler.ML\<close> |
|
12 |
ML_file \<open>am_interpreter.ML\<close> |
|
13 |
ML_file \<open>am_ghc.ML\<close> |
|
14 |
ML_file \<open>am_sml.ML\<close> |
|
15 |
ML_file \<open>report.ML\<close> |
|
16 |
ML_file \<open>compute.ML\<close> |
|
17 |
ML_file \<open>linker.ML\<close> |
|
48891 | 18 |
|
62390 | 19 |
end |