--- a/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200
@@ -12,7 +12,7 @@
("Tools/Metis/metis_translate.ML")
("Tools/Metis/metis_reconstruct.ML")
("Tools/Metis/metis_tactics.ML")
- ("Tools/try.ML")
+ ("Tools/try_methods.ML")
begin
@@ -70,10 +70,10 @@
fequal_def select_def not_atomize atomize_not_select not_atomize_select
select_FalseI
-subsection {* Try *}
+subsection {* Try Methods *}
-use "Tools/try.ML"
+use "Tools/try_methods.ML"
-setup {* Try.setup *}
+setup {* Try_Methods.setup *}
end