src/HOL/Metis.thy
changeset 46641 8801a24f9e9a
parent 46320 0b8b73b49848
child 46950 d0181abdbdac
--- a/src/HOL/Metis.thy	Fri Feb 24 11:23:33 2012 +0100
+++ b/src/HOL/Metis.thy	Fri Feb 24 11:23:34 2012 +0100
@@ -12,7 +12,7 @@
      ("Tools/Metis/metis_generate.ML")
      ("Tools/Metis/metis_reconstruct.ML")
      ("Tools/Metis/metis_tactic.ML")
-     ("Tools/try_methods.ML")
+     ("Tools/try0.ML")
 begin
 
 subsection {* Literal selection and lambda-lifting helpers *}
@@ -52,10 +52,10 @@
     select_FalseI lambda_def eq_lambdaI
 
 
-subsection {* Try Methods *}
+subsection {* Try0 *}
 
-use "Tools/try_methods.ML"
+use "Tools/try0.ML"
 
-setup {* Try_Methods.setup *}
+setup {* Try0.setup *}
 
 end