1.1 --- a/TODO.md	Wed Aug 24 19:15:06 2022 +0200
     1.2 +++ b/TODO.md	Tue Sep 06 11:47:00 2022 +0200
     1.3 @@ -65,6 +65,7 @@
     1.4  * WN: ? unify "no_met" with "empty_meth_id" from References.empty ?
     1.5  
     1.6  * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
     1.7 +  See notes in Build_Thydata.thy.
     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

     2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 19:15:06 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Sep 06 11:47:00 2022 +0200
     2.3 @@ -356,23 +356,6 @@
     2.4  \<close>
     2.5  ML \<open>
     2.6  \<close> ML \<open>
     2.7 -  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
     2.8 -\<close> ML \<open>
     2.9 -union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list;
    2.10 -merge          : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    2.11 -\<close> ML \<open>
    2.12 -val eq = op=;
    2.13 -val l1 = [1,2,3,4,5];
    2.14 -val l2 = [4,5,6,7,8];
    2.15 -\<close> ML \<open>
    2.16 -union_overwrite eq l1 l2  = [8, 7, 6, 1, 2, 3, 4, 5];
    2.17 -Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5]
    2.18 -\<close> ML \<open>
    2.19 -\<close> ML \<open>
    2.20 -Library.merge eq        (*: _a list * _a list -> _a list*);
    2.21 -curry (Library.merge eq)(*: _a list -> _a list -> _a list*)
    2.22 -\<close> ML \<open>
    2.23 -\<close> ML \<open>
    2.24  \<close> ML \<open>
    2.25  \<close>
    2.26  end

     3.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Wed Aug 24 19:15:06 2022 +0200
     3.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Tue Sep 06 11:47:00 2022 +0200
     3.3 @@ -30,8 +30,6 @@
     3.4      * type checked and marked as Type-Error
     3.5      * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)
     3.6    4. Input to 2.2 by selection from a list / tree
     3.7 -  5. On update of \<open>Problem_Ref\<close> (in the root problem) also \<open>Problem\<close> is updated;
     3.8 -     The argument of \<open>Problem\<close> comes with the template and is read-only.
     3.9  
    3.10  The specific representation of the Demo_Example demonstrate different situations
    3.11  in educational settings.