Add some methods to trym.

lib/Eval_Bool.thy

@@ -11,7 +11,7 @@
 
 theory Eval_Bool
 
-imports Main
+imports Try_Methods
 
 begin
 
@@ -47,6 +47,8 @@ method_setup eval_bool = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD'
         addsimprocs [Eval_Bool.simproc])))\<close>
     "use code generator setup to simplify booleans in goals to True or False"
 
+add_try_method eval_bool
+
 text {* Testing. *}
 definition
   eval_bool_test_seq :: "int list"

lib/Lib.thy

@@ -19,6 +19,7 @@ imports
   String_Compare
   Value_Abbreviation
   Try_Methods
+  Eval_Bool
   NICTATools
   "~~/src/HOL/Library/Prefix_Order"
 begin

lib/Try_Methods.thy

@@ -11,7 +11,7 @@
 
 theory Try_Methods
 
-imports Main
+imports Eisbach_Methods
 
 keywords "trym" :: diag
   and "add_try_method" :: thy_decl
@@ -106,11 +106,21 @@ val _ = Outer_Syntax.command @{command_keyword trym}
   (Scan.option Parse.int >> (fn opt_n =>
     Toplevel.keep_proof (try_methods_command opt_n o Toplevel.proof_of)))
 
+fun local_check_add_method nm ctxt =
+    (mk_method ctxt nm; Local_Theory.background_theory (add_method nm) ctxt)
+
 val _ = Outer_Syntax.command @{command_keyword add_try_method}
   "add a method to a library of strategies tried by trym"
-  (Parse.name >> (Toplevel.theory o add_method))
+  (Parse.name >> (Toplevel.local_theory NONE NONE o local_check_add_method))
 
 end
 *}
 
+add_try_method fastforce
+add_try_method blast
+add_try_method metis
+
+method auto_metis = solves \<open>auto; metis\<close>
+add_try_method auto_metis
+
 end