1.1 --- a/TODO.md	Tue Aug 10 11:55:24 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 12:56:06 2021 +0200
     1.3 @@ -35,9 +35,6 @@
     1.4  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
     1.5    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
     1.6  
     1.7 -* WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
     1.8 -  Is this really required, or can we just use the 'method' command?
     1.9 -
    1.10  * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.11      ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
    1.12  

     2.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Aug 10 11:55:24 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Aug 10 12:56:06 2021 +0200
     2.3 @@ -124,12 +124,10 @@
     2.4  
     2.5  subsection \<open>methods\<close>
     2.6  
     2.7 -setup \<open>KEStore_Elems.add_mets
     2.8 -    [MethodC.prep_input @{theory LinEq} "met_rootrateq" [] MethodC.id_empty
     2.9 -      (["RootRatEq"], [],
    2.10 -        {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    2.11 -          crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
    2.12 -\<close>
    2.13 +method "met_rootrateq" : "RootRatEq" =
    2.14 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    2.15 +  crls=Atools_erls, errpats = [], nrls = norm_Rational}\<close>
    2.16 +
    2.17      (*-- left 20.10.02 --*)
    2.18  partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    2.19    where

     3.1 --- a/src/Tools/isac/Knowledge/Test.thy	Tue Aug 10 11:55:24 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Tue Aug 10 12:56:06 2021 +0200
     3.3 @@ -764,12 +764,9 @@
     3.4  
     3.5  section \<open>methods\<close>
     3.6  subsection \<open>differentiate\<close>
     3.7 -setup \<open>KEStore_Elems.add_mets
     3.8 -    [MethodC.prep_input @{theory "Diff"} "met_test" [] MethodC.id_empty
     3.9 -      (["Test"], [],
    3.10 -        {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    3.11 -          crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
    3.12 -\<close>
    3.13 +method "met_test" : "Test" =
    3.14 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    3.15 +  crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
    3.16  
    3.17  partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    3.18    where