1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jun 21 20:06:12 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Jun 21 21:53:23 2021 +0200
     1.3 @@ -69,11 +69,11 @@
     1.4       ]
     1.5    | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_cas
     1.8 -  [((Thm.term_of o the o (TermC.parse @{theory})) "solveTest", 
     1.9 -      (("Test", ["univariate", "equation", "test"], ["no_met"]), argl2dtss)),
    1.10 -    ((Thm.term_of o the o (TermC.parse @{theory})) "solve",
    1.11 -      (("Isac_Knowledge", ["univariate", "equation"], ["no_met"]), argl2dtss))]\<close>
    1.12 +cas solveTest = \<open>argl2dtss\<close>
    1.13 +  Theory: Test
    1.14 +  Problem: "univariate/equation/test"
    1.15 +cas solve = \<open>argl2dtss\<close>
    1.16 +  Problem: "univariate/equation"
    1.17  
    1.18  method met_equ : "Equation" =
    1.19    \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,