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 ?