diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 40adac7..72442e0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -505,9 +505,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV- caption2="''Exploring an attribute (hyperlinked to the class).''", relative_width2="47", src2="''figures/Dogfood-V-attribute''"]\Navigation via generated hyperlinks.\ -(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure - to align them. This has to wait that the exploration of an attribute is again possible. - See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *) text\ From these class definitions, \<^isadof> also automatically generated editing diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 56646ed..bef34e0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1009,9 +1009,6 @@ text\ these types. They are just types declared in HOL, which are ``inhabited'' by special constant symbols carrying strings, for example of the format \<^boxed_theory_text>\@{thm }\. - % TODO: - % Update meta-types implementation explanation to the new implementation - % in repository commit 08c101c5440eee2a087068581952026e88c39f6a When HOL expressions were used to denote values of \<^boxed_theory_text>\doc_class\ instance attributes, this requires additional checks after