diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index fc11e20..e1916f1 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -602,6 +602,9 @@ text\ corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition (which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}). + % TODO for Burkhart Wolff. + % The last phrase should be completed to make it clearer: + % In this part "hovering over an...in order to disambiguate", something is missing. \ (* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 22caaf3..5505b38 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -177,6 +177,9 @@ text\ in \<^boxed_theory_text>\ ... \ which might contain certain ``quasi-letters'' such as \<^boxed_theory_text>\_\, \<^boxed_theory_text>\-\, \<^boxed_theory_text>\.\ (see~@{cite "wenzel:isabelle-isar:2020"} for details). + % TODO for Burkhart Wolff. + % This phrase should be reviewed to clarify identifiers. + % Peculiarly, "and identifiers in \<^boxed_theory_text>\ ... \". \<^item> \tyargs\:\<^index>\tyargs@\tyargs\\ \<^rail>\ typefree | ('(' (typefree * ',') ')')\ \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "wenzel:isabelle-isar:2020"}) @@ -282,6 +285,8 @@ text\ representations definition needs to be wrapped in a \inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context within Isabelle's \<^LaTeX>-setup. + % TODO: + % For the "(written in \<^boxed_theory_text>\\ ... \\" part, to give some examples should be clearer. Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|: \<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\renewisadof@\inlineltx{\renewisadof}\ for re-defining