1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Mon Jun 21 20:06:12 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Mon Jun 21 21:53:23 2021 +0200
     1.3 @@ -59,11 +59,10 @@
     1.4       ]
     1.5    (*| argl2dtss _ = raise ERROR "Simplify.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})) "Simplify",  
     1.9 -    (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)),
    1.10 -   ((Thm.term_of o the o (TermC.parse @{theory})) "Vereinfache",  
    1.11 -     (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
    1.12 +cas Simplify = \<open>argl2dtss\<close>
    1.13 +  Problem: "simplification"
    1.14 +cas Vereinfache = \<open>argl2dtss\<close>
    1.15 +  Problem: "vereinfachen"
    1.16  
    1.17  ML \<open>
    1.18  \<close> ML \<open>