--- a/src/HOL/Metis.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Metis.thy Wed Aug 22 22:55:41 2012 +0200
@@ -9,13 +9,10 @@
theory Metis
imports ATP
keywords "try0" :: diag
-uses "~~/src/Tools/Metis/metis.ML"
- ("Tools/Metis/metis_generate.ML")
- ("Tools/Metis/metis_reconstruct.ML")
- ("Tools/Metis/metis_tactic.ML")
- ("Tools/try0.ML")
begin
+ML_file "~~/src/Tools/Metis/metis.ML"
+
subsection {* Literal selection and lambda-lifting helpers *}
definition select :: "'a \<Rightarrow> 'a" where
@@ -41,9 +38,9 @@
subsection {* Metis package *}
-use "Tools/Metis/metis_generate.ML"
-use "Tools/Metis/metis_reconstruct.ML"
-use "Tools/Metis/metis_tactic.ML"
+ML_file "Tools/Metis/metis_generate.ML"
+ML_file "Tools/Metis/metis_reconstruct.ML"
+ML_file "Tools/Metis/metis_tactic.ML"
setup {* Metis_Tactic.setup *}
@@ -58,8 +55,7 @@
subsection {* Try0 *}
-use "Tools/try0.ML"
-
+ML_file "Tools/try0.ML"
setup {* Try0.setup *}
end