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