more scalable protocol_message: use XML.body directly (Output.output hook is not required);
(* 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