diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 99489e9..fc11e20 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -464,7 +464,11 @@ by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. hierarchy makes \<^verbatim>\X4\ \<^emph>\navigable\ in Isabelle/jedit; a click will cause the IDE to present the defining occurrence of this text-element in the integrated source. -Note, further, how \<^isadof>-commands like \<^theory_text>\text*\ interact with standard Isabelle document +% TODO: +% The definition \<^theory_text>\@{definition X4}\ is not present in the screenshot, +% it might be better to use \<^theory_text>\@{definition X22}\. + +Note, further, how \<^isadof>-commands like \<^theory_text>\text*\ interact with standard Isabelle document antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail. We refrain ourselves here to briefly describe three freeform antiquotations used her in this text: @@ -738,6 +742,12 @@ of a document get ``formal content'' and become more robust under change.\ Defining a "SRAC" in the integrated source \ldots \ +text\ +TODO: +The screenshot (figures/srac-definition) of the figure figfig5 should be updated +to have a SRAC type in uppercase. +\ + figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"] \ Using a "SRAC" as "EC" document element. \ text\ The subsequent sample in @{figure \figfig5\} shows the definition of an