1.1 --- a/TODO.md	Sat Aug 06 15:02:55 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 15:57:46 2022 +0200
     1.3 @@ -14,16 +14,6 @@
     1.4  
     1.5  ***** some items for discussion
     1.6  
     1.7 -* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
     1.8 -    https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes 
     1.9 -    several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
    1.10 -    "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
    1.11 -    knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.
    1.12 -  KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter
    1.13 -  retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) --
    1.14 -  -- get_thes and add_thes are the main reason for (b)
    1.15 -  So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
    1.16 -
    1.17  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
    1.18      ??
    1.19  
    1.20 @@ -79,7 +69,17 @@
    1.21          val ctxt = Proof_Context.init_global thy;    ->   val thy' = Context.theory_name thy
    1.22        cp code to test/*
    1.23  
    1.24 -* WN: check all Ctree.par_pblobj -- ? better get ctxt = Ctree.get_loc pt pos |> snd ?
    1.25 +* WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
    1.26 +
    1.27 +* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
    1.28 +    https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes 
    1.29 +    several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
    1.30 +    "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
    1.31 +    knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.
    1.32 +  KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter
    1.33 +  retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) --
    1.34 +  -- get_thes and add_thes are the main reason for (b)
    1.35 +  So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
    1.36  
    1.37  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.38    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";