--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Wed Aug 22 22:55:41 2012 +0200
@@ -5,7 +5,15 @@
*)
theory Compute_Oracle imports HOL
-uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
begin
+ML_file "am.ML"
+ML_file "am_compiler.ML"
+ML_file "am_interpreter.ML"
+ML_file "am_ghc.ML"
+ML_file "am_sml.ML"
+ML_file "report.ML"
+ML_file "compute.ML"
+ML_file "linker.ML"
+
end
\ No newline at end of file