| changeset 47859 | 9f492f5b0cec |
| parent 42830 | b460124855b8 |
| 47858:15ce93dfe6da | 47859:9f492f5b0cec |
|---|---|
1 (* Title: HOL/Matrix/Compute_Oracle/Compute_Oracle.thy |
|
2 Author: Steven Obua, TU Munich |
|
3 |
|
4 Steven Obua's evaluator. |
|
5 *) |
|
6 |
|
7 theory Compute_Oracle imports HOL |
|
8 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML" |
|
9 begin |
|
10 |
|
11 end |