Navigation of attributes inside "Meta-args" does not work #10

Closed
opened 2022-03-22 15:58:04 +00:00 by nicolas.meric · 0 comments
Collaborator

Example:

doc_class class_inv1 =
int1 :: "int"
invariant inv1 :: "int1 σ ≥ 3"

text*[testinv1::class_inv1, int1=4]‹lorem ipsum...›

int1 in the text* command in not clickable.

Also, update the manual accordingly:
the fig:Dogfood-IV-jumpInDocCLass side_by_side_figure images must be updated.

Example: doc_class class_inv1 = int1 :: "int" invariant inv1 :: "int1 σ ≥ 3" text*[testinv1::class_inv1, int1=4]‹lorem ipsum...› int1 in the text* command in not clickable. Also, update the manual accordingly: the fig:Dogfood-IV-jumpInDocCLass side_by_side_figure images must be updated.
Sign in to join this conversation.
No Label
No Milestone
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Isabelle_DOF/Isabelle_DOF#10
No description provided.