Spell-checking.
This commit is contained in:
parent
d3270f4afa
commit
5381182ab2
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -134,9 +134,9 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
|
|||
|
||||
It is an unique feature of \<^isadof> that ontologies may be used to control
|
||||
the link between formal and informal content in documents in a machine
|
||||
checked way. These links can connect both text elements as well as formal
|
||||
modelling elements such as terms, definitions, code and logical formulas,
|
||||
alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
checked way. These links can connect both text elements and formal
|
||||
modeling elements such as terms, definitions, code and logical formulas,
|
||||
altogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -50,7 +50,7 @@ with Standard ML (SML) at the bottom layer as implementation language. The arch
|
|||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
|
||||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>.
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
support for higher specification constructs were built.\<close>
|
||||
|
||||
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
|
||||
|
|
@ -72,7 +72,7 @@ declare_reference*["fig:dependency"::text_section]
|
|||
text\<open>
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>\<^bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
|
|
@ -103,7 +103,7 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
|
|||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
|
||||
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> parenthesis) which
|
||||
contains characters and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
|
||||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -235,7 +235,7 @@ section*[writing_doc::technical]\<open>Writing Documents: General Remarks\<close
|
|||
|
||||
subsection*[naming::example]\<open>Name-Spaces, Long- and Short-Names\<close>
|
||||
text\<open>\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were
|
||||
composed from a name of the session, the name of the theory, and a sequence of local names referring
|
||||
composed of a name of the session, the name of the theory, and a sequence of local names referring
|
||||
to, \<^eg>, nested specification constructs that were used to identify types, constant symbols,
|
||||
definitions, \<^etc>. The general format of a long-name is
|
||||
|
||||
|
|
@ -385,10 +385,10 @@ 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 focussing on its form, not refering in any sense to its content which is out of scope here.
|
||||
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,
|
||||
which is written in the so-called free-form style: Formulas are superficially parsed and
|
||||
type-setted, but no deeper type-checking and checking with the underlying logical context
|
||||
type-set, but no deeper type-checking and checking with the underlying logical context
|
||||
is undertaken. \<close>
|
||||
|
||||
figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
|
||||
|
|
@ -432,8 +432,8 @@ doc_class "theorem" = math_content +
|
|||
|
||||
|
||||
text\<open>The class \<^typ>\<open>technical\<close> regroups a number of text-elements that contain typical
|
||||
``technical content" in mathematical or engineering papers: code, definitions, theorems,
|
||||
lemmas, examples. From this class, the more stricter class of @{typ \<open>math_content\<close>} is derived,
|
||||
technical content in mathematical or engineering papers: code, definitions, theorems,
|
||||
lemmas, examples. From this class, the stricter class of @{typ \<open>math_content\<close>} is derived,
|
||||
which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these
|
||||
class definitions are omitted here). Note, however, that class identifiers can be abbreviated by
|
||||
standard \<^theory_text>\<open>type_synonym\<close>s for convenience and enumeration types can be defined by the
|
||||
|
|
@ -453,10 +453,6 @@ by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt.
|
|||
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jEdit; a click will cause the IDE to present the
|
||||
defining occurrence of this text-element in the integrated source.
|
||||
|
||||
% TODO:
|
||||
% The definition \<^theory_text>\<open>@{definition X4}\<close> is not present in the screenshot,
|
||||
% it might be better to use \<^theory_text>\<open>@{definition X22}\<close>.
|
||||
|
||||
Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> interact with standard Isabelle document
|
||||
antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail.
|
||||
We refrain ourselves here to briefly describe three freeform antiquotations used in this text:
|
||||
|
|
@ -573,7 +569,7 @@ Isabelle/jEdit will respond with an error.\<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.
|
||||
error-message and compiling a with a consistent bibtex usually makes disappear this behavior.
|
||||
\<close>
|
||||
|
||||
section*[cenelec_onto::example]\<open>Writing Certification Documents \<^boxed_theory_text>\<open>CENELEC_50128\<close>\<close>
|
||||
|
|
@ -605,7 +601,7 @@ text\<open>
|
|||
much profit from the control of ontological consistency: a substantial amount of the work
|
||||
of evaluators in formal certification processes consists in tracing down the links from
|
||||
requirements over assumptions down to elements of evidence, be it in form of semi-formal
|
||||
documentation, models, code, or tests. In a certification process, traceability becomes a major
|
||||
documentation, models, code, or tests. In a certification process, traceability becomes a major
|
||||
concern; and providing mechanisms to ensure complete traceability already at the development of
|
||||
the integrated source can in our view increase the speed and reduce the risk certification
|
||||
processes. Making the link-structure machine-checkable, be it between requirements, assumptions,
|
||||
|
|
@ -675,7 +671,7 @@ text*[ass123::SRAC]\<open>
|
|||
|
||||
This will be shown in the \<^pdf> as follows:
|
||||
\<close>
|
||||
text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer
|
||||
text*[ass123::SRAC] \<open> The overall sampling frequency of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times \ldots \<close>
|
||||
|
||||
|
|
@ -722,7 +718,7 @@ We still mention a few of these document antiquotations here:
|
|||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
||||
to a theorem; the additional ``style" argument changes the presentation by printing the
|
||||
formula into the output instead of the reference itself,
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows deriving \<open>prop\<close> on the fly, thus guarantee
|
||||
that it is a corrollary of the current context,
|
||||
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
|
||||
|
|
@ -798,7 +794,7 @@ too complex native \<^LaTeX>-commands.
|
|||
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
|
||||
create dangling references during the document generation that break the document generation.
|
||||
|
||||
Finally, we recommend to use the @{command "check_doc_global"} command at the end of your
|
||||
Finally, we recommend using the @{command "check_doc_global"} command at the end of your
|
||||
document to check the global reference structure.
|
||||
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 University of Exeter
|
||||
* 2018-2021 University of Paris-Saclay
|
||||
* 2019-2022 University of Exeter
|
||||
* 2018-2022 University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -58,7 +58,7 @@ text\<open>
|
|||
\<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated
|
||||
sources that provide textual descriptions, abbreviations, macro-support and even ML-code.
|
||||
Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close>
|
||||
organisation is slightly different and shown in
|
||||
organization is slightly different and shown in
|
||||
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>:
|
||||
%
|
||||
\begin{center}
|
||||
|
|
@ -88,9 +88,9 @@ text\<open>
|
|||
"knowledge-based" search procedures as well as tool interaction). For this reason, ontologies
|
||||
are coupled with \<^emph>\<open>layout definitions\<close> allowing an automatic mapping of an integrated
|
||||
source into \<^LaTeX> and finally \<^pdf>. The mapping of an ontology to a specific representation
|
||||
in \<^LaTeX> is steered via associated \<^LaTeX> stylefiles which were included during Isabelle's
|
||||
in \<^LaTeX> is steered via associated \<^LaTeX> style files which were included during Isabelle's
|
||||
document generation process. This mapping is potentially a one-to-many mapping;
|
||||
this implies a certain technical organisation and some resulting restrictions
|
||||
this implies a certain technical organization and some resulting restrictions
|
||||
described in @{technical (unchecked) \<open>infrastructure\<close>} in more detail.
|
||||
\<close>
|
||||
|
||||
|
|
@ -355,7 +355,7 @@ is currently only available in the SML API's of the kernel.
|
|||
| @@{command "define_macro*"} name ('\<rightleftharpoons>' | '==')
|
||||
\<newline> '\<open>' string '\<close>' '_' '\<open>' string '\<close>' \<close>
|
||||
\<close>
|
||||
text\<open>Recall that with the exception of \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
text\<open>Recall that except \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
layout (such as \<^LaTeX>); these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||
|
||||
|
|
@ -389,7 +389,7 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
|
|||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Code-Contexts and their Management\<close>
|
||||
subsection\<open>Ontological Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly:
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
|
|
@ -399,7 +399,7 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
|
|||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Term-Contexts and their Management\<close>
|
||||
subsection\<open>Ontological Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
|
||||
|
|
@ -413,7 +413,7 @@ denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> e
|
|||
executable HOL-functions to interact with meta-objects.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
\<close>
|
||||
|
|
@ -563,7 +563,7 @@ text\<open> The \<^verbatim>\<open>scholarly_paper\<close> ontology is oriented
|
|||
|
||||
It extends \<^verbatim>\<open>COL\<close> by the following concepts:
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 scholarly\_paper.title.
|
||||
|
|
@ -659,19 +659,19 @@ of the \<^isadof> language:
|
|||
text\<open>Usually, command macros for text elements will assign the generated instance
|
||||
to the default class corresponding for this class.
|
||||
For pragmatic reasons, \<^theory_text>\<open>Definition*\<close>, \<^theory_text>\<open>Lemma*\<close> and \<^theory_text>\<open>Theorem*\<close> represent an exception
|
||||
of this rule and are set up such that the default class is the super class @{typ \<open>math_content\<close>}
|
||||
to this rule and are set up such that the default class is the super class @{typ \<open>math_content\<close>}
|
||||
(rather than to the class @{typ \<open>definition\<close>}).
|
||||
This way, it is possible to use these macros for several different sorts of the very generic
|
||||
concept ``definition", which can be used as a freeform mathematical definition but also for a
|
||||
This way, it is possible to use these macros for several sorts of the very generic
|
||||
concept ``definition'', which can be used as a freeform mathematical definition but also for a
|
||||
freeform terminological definition as used in certification standards. Moreover, new subclasses
|
||||
of @{typ \<open>math_content\<close>} might be introduced in a derived ontology with an own specific layout
|
||||
definition.
|
||||
\<close>
|
||||
|
||||
text\<open>While this library is intended to give a lot of space to freeform text elements in
|
||||
order to counterbalance Isabelle's standard view, it should not be forgot that the real strength
|
||||
of Isabelle is its ability to handle both - and to establish links between both worlds.
|
||||
Therefore the formal assertion command has been integrated to capture some form of formal content.\<close>
|
||||
order to counterbalance Isabelle's standard view, it should not be forgotten that the real strength
|
||||
of Isabelle is its ability to handle both, and to establish links between both worlds.
|
||||
Therefore, the formal assertion command has been integrated to capture some form of formal content.\<close>
|
||||
|
||||
|
||||
subsubsection*["text-elements-expls"::example]\<open>Examples\<close>
|
||||
|
|
@ -742,7 +742,7 @@ high-level arranged at root-class level,
|
|||
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 technical\_report.front\_matter\DTcomment{...}.
|
||||
|
|
@ -777,7 +777,7 @@ appropriate for this type of long-and-tedious documents,
|
|||
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 CENELEC\_50128.judgement\DTcomment{...}.
|
||||
|
|
@ -924,7 +924,7 @@ val _ =
|
|||
|
||||
text\<open>
|
||||
Finally, for the document generation, a new dispatcher has to be defined in \<^LaTeX>---this is
|
||||
mandatory, otherwise the document generation will break. These dispatcher always follow the same
|
||||
mandatory, otherwise the document generation will break. These dispatchers always follow the same
|
||||
schemata:
|
||||
|
||||
\begin{ltx}
|
||||
|
|
@ -1068,7 +1068,7 @@ text\<open>
|
|||
The value of each attribute defined for the instances is checked against their classes invariants.
|
||||
As the class \<^boxed_theory_text>\<open>class_inv2\<close> is a subsclass
|
||||
of the class \<^boxed_theory_text>\<open>class_inv1\<close>, it inherits \<^boxed_theory_text>\<open>class_inv1\<close> invariants.
|
||||
Hence the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
|
||||
Hence, the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
|
||||
when the instance \<^boxed_theory_text>\<open>testinv2\<close> is defined.
|
||||
|
||||
Now let's add some invariants to our example in \<^technical>\<open>sec:example\<close>.
|
||||
|
|
@ -1157,7 +1157,7 @@ text\<open>
|
|||
header delimiting the borders of its representation. Class invariants
|
||||
on monitors allow for specifying structural properties on document
|
||||
sections.
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use the
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use
|
||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
|
||||
|
||||
|
||||
|
|
@ -1252,7 +1252,7 @@ text\<open>
|
|||
the Isabelle proof language, for example, or other more advanced concepts.
|
||||
|
||||
Technically, ontologies\<^index>\<open>ontology!directory structure\<close> are stored in a directory
|
||||
\<^boxed_bash>\<open>src/ontologies\<close> and consist of a Isabelle theory file and a \<^LaTeX>-style file:
|
||||
\<^boxed_bash>\<open>src/ontologies\<close> and consist of an Isabelle theory file and a \<^LaTeX>-style file:
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
|
|
@ -1285,7 +1285,7 @@ text\<open>
|
|||
file \<^path>\<open>src/ontologies/foo/DOF-foo.sty\<close>
|
||||
\<^item> registration (as import) of the new ontology in the file \<^path>\<open>src/ontologies/ontologies.thy\<close>.
|
||||
\<^item> activation of the new document setup by executing the install script. You can skip the lengthy
|
||||
checks for the AFP entries and the installation of the Isabelle patch by using the
|
||||
checks for the AFP entries by using the
|
||||
\<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
|
||||
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
|
||||
\<close>
|
||||
|
|
@ -1315,7 +1315,7 @@ text\<open>
|
|||
text\<open>
|
||||
Developing a new document template ``\<^boxed_bash>\<open>bar\<close>'' requires the following steps:
|
||||
\<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
|
||||
\<^item> activation of the new document template by executing the install script. You can skip the lengthy
|
||||
\<^item> activation of the new document template by executing the \<^boxed_bash>\<open>install\<close> script. You can skip the lengthy
|
||||
checks for the AFP entries and the installation of the Isabelle patch by using the
|
||||
\<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
|
||||
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
|
||||
|
|
@ -1390,7 +1390,7 @@ text\<open>
|
|||
|
||||
subsubsection\<open>Getting Started\<close>
|
||||
text\<open>
|
||||
In general, we recommend to create a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
|
||||
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
|
||||
to develop new document templates or ontology representations. The default setup of the \<^isadof>
|
||||
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
|
||||
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:
|
||||
|
|
@ -1468,8 +1468,8 @@ The new command \<^boxed_latex>\<open>\addauthor\<close> and a similarly defined
|
|||
can now be used in the definition of the representation of the concept
|
||||
\<^boxed_theory_text>\<open>text.scholarly_paper.author\<close>, which writes the collected information in the
|
||||
job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary,
|
||||
as the author and affiliation information is required right at the begin of the document
|
||||
while \<^isadof> allows to define authors at any place within a document:
|
||||
as the author and affiliation information is required right at the beginning of the document
|
||||
while \<^isadof> allows defining authors at any place within a document:
|
||||
|
||||
\begin{ltx}
|
||||
\provideisadof{text.scholarly_paper.author}%
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 University of Exeter
|
||||
* 2018-2021 University of Paris-Saclay
|
||||
* 2019-2022 University of Exeter
|
||||
* 2018-2022 University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -92,7 +92,7 @@ op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
|
|||
op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
|
||||
op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
|
||||
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
|
||||
combinators have the advantage that they can be smoothlessly integrated into standard programs,
|
||||
combinators have the advantage that they can be integrated into standard programs,
|
||||
and they enable the dynamic extension of the grammar. There is a more high-level structure
|
||||
\inlinesml{Parse} providing specific combinators for the command-language Isar:
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue