pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

added a remark on @{cite ...}

This commit is contained in:
Burkhart Wolff 2022-03-20 19:02:14 +01:00
parent d86173834f
commit fb91700a43
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -552,7 +552,11 @@ text\<open>At times, this causes idiosyncrasies like the ones cited in the follo
not equivalent \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen''A \isasymlongrightarrow\ B''\isasymclose\<close> (fails).
\<close>
text\<open>We advise users to experiment with different notation variants.\<close>
text\<open>We advise users to experiment with different notation variants.
Note, further, that the Isabelle \<^latex>\<open>@\{cite ...\}\<close>-text-anti-quotation makes its checking
on the level of generated \<^verbatim>\<open>.aux\<close>-files, which are not necessarily up-to-date. Ignoring the PIDE
error-message and compiling a with a consistent bibtex usually makes disappear this behaviour.
\<close>
section*[cenelec_onto::example]\<open>Writing Certification Documents (CENELEC\_50128)\<close>
subsection\<open>The CENELEC 50128 Example\<close>