1.1 --- a/src/Tools/isac/TODO.thy	Wed May 20 12:52:09 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Sun May 24 16:05:36 2020 +0200
     1.3 @@ -27,6 +27,14 @@
     1.4  (*\------- to  from -------/*)
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 +  \item LibraryC.distinct shadows Library.distinct (+ seeLibrary.member)
     1.8 +  \item xxx
     1.9 +  \item Specify.find_next_step: References.select
    1.10 +    cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
    1.11 +                                      ^^^^^  Problem.id
    1.12 +  \item xxx
    1.13 +  \item Calc.state_empty_post \<rightarrow> Calc.state_post_empty
    1.14 +  \item xxx
    1.15    \item distribute code from test/../calchead.sml
    1.16    \item xxx
    1.17    \item rename Tactic.Calculate -> Tactic.Evaluate
    1.18 @@ -54,6 +62,9 @@
    1.19  text \<open>
    1.20    \begin{itemize}
    1.21    \item xxx
    1.22 +  \item Isa20.implementation: 0.2.4 Printing ML values ?INSTEAD? *.TO_STRING ???
    1.23 +    ??? writeln ( make_string {x = x, y = y}); ???
    1.24 +  \item xxx
    1.25    \item revise O_Model and I_Model with an example with more than 1 variant.
    1.26    \item xxx
    1.27    \item ctxt is superfluous in specify-phase due to type constraints from Descript.thy