tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;
(* Title: HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
Author: Steven Obua, TU Munich
Steven Obua's evaluator.
*)
theory Compute_Oracle imports HOL.HOL
begin
ML_file \<open>am.ML\<close>
ML_file \<open>am_compiler.ML\<close>
ML_file \<open>am_interpreter.ML\<close>
ML_file \<open>am_ghc.ML\<close>
ML_file \<open>am_sml.ML\<close>
ML_file \<open>report.ML\<close>
ML_file \<open>compute.ML\<close>
ML_file \<open>linker.ML\<close>
end