1.1 --- a/TODO.md	Tue Aug 10 09:43:07 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 10:27:15 2021 +0200
     1.3 @@ -78,3 +78,7 @@
     1.4  * WN: reduce the number of TermC.parse*;
     1.5    + 0d22a6bf1fc6 was too much for 1 changeset
     1.6    + first parse with ctxt in Specify (O_Model.init shall return a context,..) etc
     1.7 +
     1.8 +* WN: push initiatives of MW through the whole code
     1.9 +  + e1da148725ed : \<^ML>\<open>...\<close> instead parentheses
    1.10 +  + 
    1.11 \ No newline at end of file

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Aug 10 09:43:07 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Aug 10 10:27:15 2021 +0200
     2.3 @@ -28,6 +28,20 @@
     2.4    In contrast, old-style \<^ML>\<open>Thy_Info.get_theory\<close> requires a finished logic image, for
     2.5    example in \<^file>\<open>$ISABELLE_ISAC_TEST/Tools/isac/Test_Some.thy\<close> loaded from session Isac.
     2.6  
     2.7 +  Note on planned improvements (WN): 
     2.8 +  All theories below ML_structure\<open>MathEngine\<close> in the sessiongraph
     2.9 +  can be considered as Isac's version of Pure: the respective code handles items
    2.10 +  declared later between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
    2.11 +  These items are contained in the  ML_structure\<open>Context\<close> in current Isabelle,
    2.12 +  thus all ML_structure\<open>KEStore_Elems\<close> can be replaced by more native Isabelle mechanisms --
    2.13 +  with two exceptions
    2.14 +    \<^item> \<^ML>\<open>KEStore_Elems.add_pbts\<close> and \<^ML>\<open>KEStore_Elems.get_ptyps\<close>, 
    2.15 +      handling a tree of \<^ML_type>\<open>Problem.T\<close>
    2.16 +    \<^item> \<^ML>\<open>KEStore_Elems.add_mets\<close> and \<^ML>\<open>KEStore_Elems.get_mets\<close>, 
    2.17 +      handling a tree of \<^ML_type>\<open>MethodC.T\<close>
    2.18 +  where both trees have a structure independent from the dependency graph 
    2.19 +  between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
    2.20 +
    2.21  \<close>
    2.22  subsubsection \<open>Get and group the theories defined in Isac\<close>
    2.23  ML \<open>
    2.24 @@ -57,6 +71,8 @@
    2.25  ML \<open>
    2.26  map Context.theory_name progthys'
    2.27  \<close> ML \<open>
    2.28 +[] : MethodC.T list
    2.29 +\<close> ML \<open>
    2.30  \<close>
    2.31  
    2.32  subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>