# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1662457620 -7200
# Node ID 263cd9e479918b87ae6a716da45870e1a3ff1d93
# Parent  432c3bbc95c34549bfdede1e22684d2a88517207
prepare elimination of KEStore_Elems.get_thes, add_thes

diff -r 432c3bbc95c3 -r 263cd9e47991 TODO.md
--- a/TODO.md	Wed Aug 24 19:15:06 2022 +0200
+++ b/TODO.md	Tue Sep 06 11:47:00 2022 +0200
@@ -65,6 +65,7 @@
 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ?
 
 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
+  See notes in Build_Thydata.thy.
     https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes 
     several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
     "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
diff -r 432c3bbc95c3 -r 263cd9e47991 src/Tools/isac/BaseDefinitions/Know_Store.thy
--- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Aug 24 19:15:06 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Sep 06 11:47:00 2022 +0200
@@ -356,23 +356,6 @@
 \<close>
 ML \<open>
 \<close> ML \<open>
-  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
-\<close> ML \<open>
-union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list;
-merge          : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
-\<close> ML \<open>
-val eq = op=;
-val l1 = [1,2,3,4,5];
-val l2 = [4,5,6,7,8];
-\<close> ML \<open>
-union_overwrite eq l1 l2  = [8, 7, 6, 1, 2, 3, 4, 5];
-Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5]
-\<close> ML \<open>
-\<close> ML \<open>
-Library.merge eq        (*: _a list * _a list -> _a list*);
-curry (Library.merge eq)(*: _a list -> _a list -> _a list*)
-\<close> ML \<open>
-\<close> ML \<open>
 \<close> ML \<open>
 \<close>
 end
diff -r 432c3bbc95c3 -r 263cd9e47991 src/Tools/isac/BridgeJEdit/VSCode_Example.thy
--- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Wed Aug 24 19:15:06 2022 +0200
+++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Tue Sep 06 11:47:00 2022 +0200
@@ -30,8 +30,6 @@
     * type checked and marked as Type-Error
     * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)
   4. Input to 2.2 by selection from a list / tree
-  5. On update of \<open>Problem_Ref\<close> (in the root problem) also \<open>Problem\<close> is updated;
-     The argument of \<open>Problem\<close> comes with the template and is read-only.
 
 The specific representation of the Demo_Example demonstrate different situations
 in educational settings.