src/Tools/isac/TODO.thy
changeset 59934 955d6fa8bb9b
parent 59933 92214be419b2
child 59935 16927a749dd7
     1.1 --- a/src/Tools/isac/TODO.thy	Mon May 04 10:19:16 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Mon May 04 11:13:16 2020 +0200
     1.3 @@ -54,6 +54,9 @@
     1.4  text \<open>
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 +  \item Derive.do_one: TODO find code in common with complete_solve
     1.8 +        Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
     1.9 +  \item xxx
    1.10    \item Solve_Check: postponed parsing input to _ option
    1.11    \item xxx
    1.12    \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?