Delete some TODOs, now done, in the manual
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-08 12:06:28 +02:00
parent a331b80095
commit 17df6a271b
2 changed files with 0 additions and 6 deletions

View File

@ -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''"]\<open>Navigation via generated hyperlinks.\<close>
(* 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\<open>
From these class definitions, \<^isadof> also automatically generated editing

View File

@ -1009,9 +1009,6 @@ text\<open>
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>\<open>@{thm <string>}\<close>.
% 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>\<open>doc_class\<close>
instance attributes, this requires additional checks after