src/HOL/Metis.thy
changeset 46641 8801a24f9e9a
parent 46320 0b8b73b49848
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/Metis.thy	Fri Feb 24 11:23:33 2012 +0100
     1.2 +++ b/src/HOL/Metis.thy	Fri Feb 24 11:23:34 2012 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4       ("Tools/Metis/metis_generate.ML")
     1.5       ("Tools/Metis/metis_reconstruct.ML")
     1.6       ("Tools/Metis/metis_tactic.ML")
     1.7 -     ("Tools/try_methods.ML")
     1.8 +     ("Tools/try0.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Literal selection and lambda-lifting helpers *}
    1.12 @@ -52,10 +52,10 @@
    1.13      select_FalseI lambda_def eq_lambdaI
    1.14  
    1.15  
    1.16 -subsection {* Try Methods *}
    1.17 +subsection {* Try0 *}
    1.18  
    1.19 -use "Tools/try_methods.ML"
    1.20 +use "Tools/try0.ML"
    1.21  
    1.22 -setup {* Try_Methods.setup *}
    1.23 +setup {* Try0.setup *}
    1.24  
    1.25  end