Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Linting ...

This commit is contained in:
Achim D. Brucker 2024-04-26 07:00:44 +01:00
parent 55e42142fa
commit 9feeb63665
7 changed files with 46 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Isabelle_DOF/ontologies/technical_report/technical_report.thy
View File

@ -169,7 +169,7 @@ lemma drc_acyclic : "acyclic doc_class_rel"
cid_of listing := 1, cid_of figure := 1, cid_of proposition := 1)"
show ?thesis
unfolding doc_class_rel_def
apply(rule_tac f = "?measure" in acyclicI_order)
apply(rule acyclicI_order [where f = "?measure"])
by(simp only: class_ids)(auto)
qed

16
Isabelle_DOF/thys/manual/M_01_Introduction.thy
View File

@ -24,17 +24,17 @@ The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\
digitization of knowledge and its propagation. This challenge incites numerous research efforts
summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic''
text processing. A key role in structuring this linking plays is \<^emph>\<open>document ontologies\<close> (also called
\<^emph>\<open>vocabulary\<close> in the semantic web community~@{cite "w3c:ontologies:2015"}), \<^ie>, a machine-readable
\<^emph>\<open>vocabulary\<close> in the semantic web community~\<^cite>\<open>"w3c:ontologies:2015"\<close>), \<^ie>, a machine-readable
form of the structure of documents as well as the document discourse.
Such ontologies can be used for the scientific discourse within scholarly articles, mathematical
libraries, and in the engineering discourse of standardized software certification
documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. All these
documents~\<^cite>\<open>"boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"\<close>. All these
documents contain formal content and have to follow a given structure. In practice, large groups of developers have to produce a substantial
set of documents where consistency is notoriously difficult to maintain. In particular,
certifications are centred around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
set of documents. While technical solutions for the traceability problem exist (most notably:
DOORS~@{cite "ibm:doors:2019"}), they are weak in the treatment of formal entities (such as formulas
DOORS~\<^cite>\<open>"ibm:doors:2019"\<close>), they are weak in the treatment of formal entities (such as formulas
and their logical contexts).
Further applications are the domain-specific discourse in juridical texts or medical reports.
@ -53,7 +53,7 @@ the Document Ontology Framework (\<^dof>) and an implementation of \<^dof> calle
provers. \<^isadof> is an instance of this novel framework, implemented as an extension of Isabelle/HOL,
to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them during document evolution. Based on Isabelle's
infrastructures, ontologies may refer to types, terms, proven theorems, code, or established
assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}),
assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, \<^cite>\<open>"wenzel:asynchronous:2014"\<close>),
a document is checked to be \<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast
user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in the case of document
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can
@ -63,7 +63,7 @@ To avoid any misunderstanding: \<^isadof> is \<^emph>\<open>not a theory in HOL
track and trace links in texts. It is an \<^emph>\<open>environment to write structured text\<close> which
\<^emph>\<open>may contain\<close> Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However,
into the Isabelle/Isar framework in the style of~\<^cite>\<open>"wenzel.ea:building:2007"\<close>. However,
\<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
and code that allows both interactive checking and formal reasoning over meta-data
related to annotated documents.\<close>
@ -113,7 +113,7 @@ CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src\<close
subsubsection\<open>How to Cite \<^isadof>\<close>
text\<open>
If you use or extend \<^isadof> in your publications, please use
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
\<^item> for the \<^isadof> system~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>:
\begin{quote}\small
A.~D. Brucker, I.~Ait-Sadoune, N. Méric, and B.~Wolff. Using Deep Ontologies in Formal
Software Engineering. In \<^emph>\<open>International Conference on Rigorous State-Based Methods (ABZ 2023)\<close>,
@ -122,7 +122,7 @@ text\<open>
\end{quote}
A \<^BibTeX>-entry is available at:
\<^url>\<open>https://www.lri.fr/~wolff/bibtex/wolff.html\<close>.
\<^item> an older description of the system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
\<^item> an older description of the system~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>:
\begin{quote}\small
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
framework: Linking the formal with the informal. In \<^emph>\<open>Conference on Intelligent Computer
@ -132,7 +132,7 @@ text\<open>
\end{quote}
A \<^BibTeX>-entry is available at:
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018\<close>.
\<^item> for the implementation of \<^isadof>~@{cite "brucker.ea:isabelledof:2019"}:
\<^item> for the implementation of \<^isadof>~\<^cite>\<open>"brucker.ea:isabelledof:2019"\<close>:
\begin{quote}\small
A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in

20
Isabelle_DOF/thys/manual/M_02_Background.thy
View File

@ -27,17 +27,17 @@ figure*[architecture::figure,relative_width="95",file_src="''figures/isabelle-ar
text*[bg::introduction]\<open>
While Isabelle is widely perceived as an interactive theorem
prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize
prover for HOL (Higher-order Logic)~\<^cite>\<open>"nipkow.ea:isabelle:2002"\<close>, we would like to emphasize
the view that Isabelle is far more than that: it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>. This
refers to the ``\<^emph>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.
Among other things, Isabelle provides an infrastructure for Isabelle plug-ins, comprising extensible
state components and extensible syntax that can be bound to SML programs. Thus, the Isabelle
architecture may be understood as an extension and refinement of the traditional `LCF approach',
with explicit infrastructure for building derivative systems.\<close>''~@{cite "wenzel.ea:building:2007"}
with explicit infrastructure for building derivative systems.\<close>''~\<^cite>\<open>"wenzel.ea:building:2007"\<close>
The current system framework offers moreover the following features:
\<^item> a build management grouping components into to pre-compiled sessions,
\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends,
\<^item> a prover IDE (PIDE) framework~\<^cite>\<open>"wenzel:asynchronous:2014"\<close> with various front-ends,
\<^item> documentation-generation,
\<^item> code generators for various target languages,
\<^item> an extensible front-end language Isabelle/Isar, and,
@ -151,7 +151,7 @@ to switch from a text-context to a term-context, for example. Therefore, antiquo
literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
Isabelle comes with a number of built-in antiquotations for text- and code-contexts;
a detailed overview can be found in @{cite "wenzel:isabelle-isar:2020"}. \<^dof> reuses this general
a detailed overview can be found in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. \<^dof> reuses this general
infrastructure but \<^emph>\<open>generates\<close> its own families of antiquotations from ontologies.\<close>
text\<open> An example for a text-element \<^index>\<open>text-element\<close> using built-in antoquotations
@ -203,19 +203,19 @@ text\<open>
(protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or Coq
and its derivatives. \<^dof> is, however, designed for fast interaction in an IDE. If a user wants
to benefit from this experience, only Isabelle and Coq have the necessary infrastructure of
asynchronous proof-processing and support by a PIDE~@{cite "wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which
asynchronous proof-processing and support by a PIDE~\<^cite>\<open>"wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"\<close> which
in many features over-accomplishes the required features of \<^dof>.
\<close>
figure*["fig_dof_ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\<open>
The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page
of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
of~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>.\<close>
text\<open>
We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> .
@{figure "fig_dof_ide"} shows a screenshot of an introductory paper on
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
\<^isadof>~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>: the \<^isadof> PIDE can be seen on the left,
while the generated presentation in PDF is shown on the right.
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits.
@ -223,8 +223,8 @@ text\<open>
mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous
evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE
evaluation and checking of the document content~\<^cite>\<open>"wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013"\<close> and is dynamically extensible. Its PIDE
provides a \<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and
auto-completion. It also provides infrastructure for displaying meta-information (\<^eg>, binding
and type annotation) as pop-ups, while hovering over sub-expressions. A fine-grained dependency

10
Isabelle_DOF/thys/manual/M_03_GuidedTour.thy
View File

@ -74,12 +74,12 @@ is currently consisting out of three AFP entries:
contains the \<^isadof> system itself, including the \<^isadof> manual.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-I\<close>: This entry contains an example of
an academic paper written using the \<^isadof> system oriented towards an
introductory paper. The text is based on~@{cite "brucker.ea:isabelle-ontologies:2018"};
introductory paper. The text is based on~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>;
in the document, we deliberately refrain from integrating references to formal content in order
to demonstrate that \<^isadof> can be used for writing documents with very little direct use of
\<^LaTeX>.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of
a mathematics-oriented academic paper. It is based on~@{cite "taha.ea:philosophers:2020"}.
a mathematics-oriented academic paper. It is based on~\<^cite>\<open>"taha.ea:philosophers:2020"\<close>.
It represents a typical mathematical text, heavy in definitions with complex mathematical notation
and a lot of non-trivial cross-referencing between statements, definitions, and proofs which
are ontologically tracked. However, with respect to the possible linking between the underlying formal theory
@ -289,7 +289,7 @@ contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \
subsection\<open>Writing Academic Publications: A Freeform Mathematics Text \<close>
text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
paper focusing on its form, not referring in any sense to its content which is out of scope here.
As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose,
As mentioned before, we chose the paper~\<^cite>\<open>"taha.ea:philosophers:2020"\<close> for this purpose,
which is written in the so-called free-form style: Formulas are superficially parsed and
type-set, but no deeper type-checking and checking with the underlying logical context
is undertaken. \<close>
@ -629,7 +629,7 @@ text\<open> This is *\<open>emphasized\<close> and this is a
citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
\<close>}
The list of standard Isabelle document antiquotations, as well as their options and styles,
can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"},
can be found in the Isabelle reference manual \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
section 4.2.
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
@ -638,7 +638,7 @@ not possible. As far as possible, raw \<^LaTeX> should be restricted to the defi
of ontologies and macros (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}). If raw
\<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
\<^latex>\<open>\verb+\+\verb+<^latex>+\<close>\<open>\<open>argument\<close>\<close> to isolate these parts
(cf. @{cite "wenzel:isabelle-isar:2020"}).
(cf. \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can

2
Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy
View File

@ -176,7 +176,7 @@ proof(induct S)
then show ?case by simp
next
case (Cons a S)
then show ?case apply(auto)
then show ?case apply(auto)[1]
using concatWith.elims apply blast
using concatWith.elims apply blast
using list.set_cases by force

36
Isabelle_DOF/thys/manual/M_06_RefMan.thy
View File

@ -119,7 +119,7 @@ text\<open>
\<^item> attributes may have default values in order to facilitate notation.
\<^boxed_theory_text>\<open>doc_class\<close>'es and \<^boxed_theory_text>\<open>onto_class\<close>'es respectively, have a semantics,
\<^ie>, a logical representation as extensible records in HOL (@{cite "wenzel:isabelle-isar:2020"},
\<^ie>, a logical representation as extensible records in HOL (\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
pp. 11.6); there are therefore amenable to logical reasoning.
\<close>
@ -169,25 +169,25 @@ text\<open>
As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily
mixed with standard HOL specification constructs. To make this manual self-contained, we present
syntax and semantics of the specification constructs that are most likely relevant for the
developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}). Our
developer of ontologies (for more details, see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>). Our
presentation is a simplification of the original sources following the needs of ontology developers
in \<^isadof>:
\<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close>
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
(called \<open>short_ident\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
(called \<open>short_ident\<close>'s in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>) and identifiers
in \<^boxed_theory_text>\<open>...\<close> which might contain certain ``quasi-letters'' such
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close> for
details).
% TODO
% This phrase should be reviewed to clarify identifiers.
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
\<open>typefree\<close> denotes fixed type variable (\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
\<open>typefree\<close> denotes fixed type variable (\<open>'a\<close>, \<open>'b\<close>, ...) (see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>)
\<^item> \<open>dt_name\<close>:\<^index>\<open>dt\_npurdahame@\<open>dt_name\<close>\<close>
\<^rail>\<open> (tyargs?) name (mixfix?)\<close>
The syntactic entity \<open>name\<close> denotes an identifier, \<open>mixfix\<close> denotes the usual
parenthesized mixfix notation (see @{cite "wenzel:isabelle-isar:2020"}).
parenthesized mixfix notation (see \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
The \<^emph>\<open>name\<close>'s referred here are type names such as \<^typ>\<open>int\<close>, \<^typ>\<open>string\<close>,
\<^type>\<open>list\<close>, \<^type>\<open>set\<close>, etc.
\<^item> \<open>type_spec\<close>:\index{type_spec@\<open>type_spec\<close>}
@ -212,13 +212,13 @@ text\<open>
% Show string in the document output for \<^boxed_theory_text>\<open>ab c\<close> (strings)
\<^boxed_theory_text>\<open>{1,2,3}\<close> (sets), \<^boxed_theory_text>\<open>(1,2,3)\<close> (tuples),
\<^boxed_theory_text>\<open>\<forall> x. P(x) \<and> Q x = C\<close> (formulas). For comprehensive overview,
see~@{cite "nipkow:whats:2020"}.
see~\<^cite>\<open>"nipkow:whats:2020"\<close>.
\<close>
text\<open>
Advanced ontologies can, \<^eg>, use recursive function definitions with
pattern-matching~@{cite "kraus:defining:2020"}, extensible record
specifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations.
pattern-matching~\<^cite>\<open>"kraus:defining:2020"\<close>, extensible record
specifications~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>, and abstract type declarations.
\<close>
text\<open>\<^isadof> works internally with fully qualified names in order to avoid confusions
@ -290,7 +290,7 @@ text\<open>
class representation, the identifier \<^boxed_latex>\<open>#1\<close> refers to the content of the main text of the
document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced
by their name using the \<^ltxinline>\<open>\commandkey{...}\<close>-command (see the documentation of the
\<^LaTeX>-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
\<^LaTeX>-package ``keycommand''~\<^cite>\<open>"chervet:keycommand:2010"\<close> for details). Usually, the
representations definition needs to be wrapped in a
\<^ltxinline>\<open>\begin{isarmarkup}...\end{isamarkup}\<close>-environment, to ensure the correct context
within Isabelle's \<^LaTeX>-setup.
@ -353,7 +353,7 @@ text\<open>
as specified in @{technical \<open>odl_manual0\<close>}.
\<^item> \<open>meta_args\<close> :
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
\<^item> \<^emph>\<open>evaluator\<close>: from \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>, evaluation is tried first using ML,
falling back to normalization by evaluation if this fails. Alternatively a specific
evaluator can be selected using square brackets; typical evaluators use the
current set of code equations to normalize and include \<open>simp\<close> for fully
@ -433,7 +433,7 @@ term antiquotations:
will get the value of the \<^const>\<open>definition_list\<close> attribute of the instance \<open>odl-manual1\<close>.
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
\<^theory_text>\<open>@{value_ [nbe] \<open>definition_list @{technical \<open>odl-manual1\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
the term using normalization by evaluation (see @{cite "wenzel:isabelle-isar:2020"}).
the term using normalization by evaluation (see \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
\<close>
(*<*)
@ -514,7 +514,7 @@ with the \<^boxed_theory_text>\<open>disable_assert_evaluation\<close> theory at
Then @{command "assert*"} will act like @{command "term*"}.
The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
(see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain
(see the @{command "definition"} command in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>) to contain
term-antiquotations. For example:
@{boxed_theory_text [display]
\<open>doc_class A =
@ -525,7 +525,7 @@ definition*[a1::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a
The @{term_ [source] \<open>@{A \<open>a1\<close>}\<close>} term-antiquotation is used both in \<open>prop\<close> and in \<open>spec_prems\<close>.
@{command "lemma*"}, @{command "theorem*"}, etc., are extended versions of the goal commands
defined in @{cite "wenzel:isabelle-isar:2020"}. Term-antiquotations can be used either in
defined in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. Term-antiquotations can be used either in
a \<open>long_statement\<close> or in a \<open>short_statement\<close>.
For instance:
@{boxed_theory_text [display]
@ -960,7 +960,7 @@ subsubsection\<open>For Isabelle Hackers: Defining New Top-Level Commands\<close
text\<open>
Defining such new top-level commands requires some Isabelle knowledge as well as
extending the dispatcher of the \<^LaTeX>-backend. For the details of defining top-level
commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2020"}.
commands, we refer the reader to the Isar manual~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>.
Here, we only give a brief example how the \<^boxed_theory_text>\<open>section*\<close>-command is defined; we
refer the reader to the source code of \<^isadof> for details.
@ -1157,7 +1157,7 @@ text\<open>
The \<^boxed_theory_text>\<open>\<sigma>\<close> symbol is reserved and references the future instance class.
By relying on the implementation of the Records
in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
in Isabelle/HOL~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
one can reference an attribute of an instance using its selector function.
For example, \<^boxed_theory_text>\<open>int1 \<sigma>\<close> denotes the value
of the \<^boxed_theory_text>\<open>int1\<close> attribute
@ -1542,8 +1542,8 @@ text\<open>
Examples of this can be found, \<^eg>, in the ontology-style
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>.
For details about the expansion mechanism
in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~@{cite "knuth:texbook:1986"
and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"}).
in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~\<^cite>\<open>"knuth:texbook:1986"
and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"\<close>).
\<close>

6
Isabelle_DOF/thys/manual/M_07_Implementation.thy
View File

@ -33,7 +33,7 @@ text\<open>
\<close>
text\<open>
Semantic macros, as required by our document model, are called \<^emph>\<open>document antiquotations\<close>
in the Isabelle literature~@{cite "wenzel:isabelle-isar:2020"}. While Isabelle's code-antiquotations
in the Isabelle literature~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. While Isabelle's code-antiquotations
are an old concept going back to Lisp and having found via SML and OCaml their ways into modern
proof systems, special annotation syntax inside documentation comments have their roots in
documentation generators such as Javadoc. Their use, however, as a mechanism to embed
@ -210,13 +210,13 @@ text\<open>
possible;
otherwise, if \<^boxed_sml>\<open>next\<close> fails, an error is reported. The automata implementation
is, in large parts, generated from a formalization of functional automata
@{cite "nipkow.ea:functional-Automata-afp:2004"}.
\<^cite>\<open>"nipkow.ea:functional-Automata-afp:2004"\<close>.
\<close>
section\<open>The \<^LaTeX>-Core of \<^isadof>\<close>
text\<open>
The \<^LaTeX>-implementation of \<^isadof> heavily relies on the
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \<^LaTeX>-commands
``keycommand''~\<^cite>\<open>"chervet:keycommand:2010"\<close> package. In fact, the core \<^isadof> \<^LaTeX>-commands
are just wrappers for the corresponding commands from the keycommand package:
@{boxed_latex [display]