
diff -r 21b6baec55b1 -r 42330f25142c src/HOL/Metis.thy
--- 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




