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

Updated Isabelle version.

This commit is contained in:
Achim D. Brucker 2020-04-08 21:40:34 +01:00
parent 968694f153
commit 358be52b61
8 changed files with 26 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@ -21,7 +21,7 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u
Isabelle/DOF has two major pre-requisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020-RC4/).
Please download the Isabelle 2019 distribution for your operating
Please download the Isabelle 2020 distribution for your operating
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020-RC4/).
* **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This
is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later)

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

@ -51,7 +51,7 @@ subsubsection*[prerequisites::technical]\<open>Pre-requisites\<close>
text\<open>
\isadof has to major pre-requisites:
\<^item> \<^bold>\<open>Isabelle\<close>\bindex{Isabelle} (\isabellefullversion).
\isadof uses a two-part version system (e.g., 1.0.0/2019),
\isadof uses a two-part version system (e.g., 1.0.0/2020),
where the first part is the version of \isadof (using semantic versioning) and the second
part is the supported version of Isabelle. Thus, the same version of \isadof might be
available for different versions of Isabelle.
@ -266,7 +266,7 @@ users are:
\<^item> The file \inlinebash|ROOT|\index{ROOT}, which defines the Isabelle session. New theory files as well as new
files required by the document generation (\eg, images, bibliography database using \BibTeX, local
\LaTeX-styles) need to be registered in this file. For details of Isabelle's build system, please
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2019"}.
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
\<^item> The file \inlinebash|praemble.tex|\index{praemble.tex}, which allows users to add additional
\LaTeX-packages or to add/modify \LaTeX-commands.
\<close>
@ -552,7 +552,7 @@ figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''
\<open> Standard antiquotations referring to theory elements.\<close>
text\<open> The corresponding view in @{docitem_ref \<open>figfig3\<close>} shows core part of a document
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
@{cite "wenzel:isabelle-isar:2019"} into formal entities of a theory. This way, the informal parts
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
of a document get ``formal content'' and become more robust under change.\<close>
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]

18
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -220,22 +220,22 @@ 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:2019"}. Our
developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}. Our
presentation is a simplification of the original sources following the needs of ontology developers
in \isadof:
\<^item> \<open>name\<close>:\index{name@\<open>name\<close>}
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2019"}) and identifiers
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such
as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2019"} for
as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2020"} for
details).
\<^item> \<open>tyargs\<close>:\index{tyargs@\<open>tyargs\<close>}
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2019"})
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
\<^item> \<open>dt_name\<close>:\index{dt\_npurdahame@\<open>dt_name\<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:2019"}).
parenthesized mixfix notation (see @{cite "wenzel:isabelle-isar:2020"}).
The \<open>name\<close>'s referred here are type names such as \<^verbatim>\<open>int\<close>, \<^verbatim>\<open>string\<close>, \<^verbatim>\<open>list\<close>, \<^verbatim>\<open>set\<close>, etc.
\<^item> \<open>type_spec\<close>:\index{type_spec@\<open>type_spec\<close>}
\<^rail>\<open> (tyargs?) name\<close>
@ -256,13 +256,13 @@ text\<open>
mathematical notations for $\lambda$-terms in Isabelle/HOL. Example expressions are:
\inlineisar|1+2| (arithmetics), \inlineisar|[1,2,3]| (lists), \inlineisar|''ab c''| (strings),
\inlineisar|{1,2,3}| (sets), \inlineisar|(1,2,3)| (tuples),
\inlineisar|\<forall> x. P(x) \<and> Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2019"}.
\inlineisar|\<forall> x. P(x) \<and> Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2020"}.
\<close>
text\<open>
Advanced ontologies can, \eg, use recursive function definitions with
pattern-matching~@{cite "kraus:defining:2019"}, extensible record
pecifications~@{cite "wenzel:isabelle-isar:2019"}, and abstract type declarations.
pattern-matching~@{cite "kraus:defining:2020"}, extensible record
pecifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations.
\<close>
text\<open>Note that \isadof works internally with fully qualified names in order to avoid
@ -554,7 +554,7 @@ subsubsection\<open>Experts: 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:2019"}.
commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2020"}.
Here, we only give a brief example how the \inlineisar|section*|-command is defined; we
refer the reader to the source code of \isadof for details.

2
examples/technical_report/Isabelle_DOF-Manual/05_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:2019"}. While Isabelle's code-antiquotations
in the Isabelle literature~@{cite "wenzel:isabelle-isar:2020"}. 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

18
examples/technical_report/Isabelle_DOF-Manual/document/root.bib
View File

@ -17,10 +17,10 @@
year = 2019
}
@Manual{ wenzel:isabelle-isar:2019,
@Manual{ wenzel:isabelle-isar:2020,
title = {The Isabelle/Isar Reference Manual},
author = {Makarius Wenzel},
year = 2019,
year = 2020,
note = {Part of the Isabelle distribution.}
}
@ -41,7 +41,7 @@
ontological feedback during the editing of a document.
In this paper, we give an in-depth presentation of the
design concepts of DOF{\^a}s Ontology Definition Language
design concepts of DOF's Ontology Definition Language
(ODL) and key aspects of the technology of its
implementation. Isabelle/DOF is the first ontology language
supporting machine-checked links between the formal and
@ -321,18 +321,18 @@
year = 2019
}
@Misc{ kraus:defining:2019,
@Misc{ kraus:defining:2020,
title = {Defining Recursive Functions in Isabelle/HOL},
author = {Alexander Kraus},
note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}},
year = 2019
year = 2020
}
@Misc{ nipkow:whats:2019,
@Misc{ nipkow:whats:2020,
title = {What's in Main},
author = {Tobias Nipkow},
note = {\url{https://isabelle.in.tum.de/doc/main.pdf}},
year = 2019
year = 2020
}
@InProceedings{ wenzel:system:2014,
@ -455,10 +455,10 @@
year = 2019
}
@Booklet{ wenzel:system-manual:2019,
@Booklet{ wenzel:system-manual:2020,
author = {Makarius Wenzel},
title = {The {Isabelle} System Manual},
year = 2019,
year = 2020,
note = {Part of the Isabelle distribution.}
}

2
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -21,7 +21,7 @@ open_monitor*[this::report]
(*>*)
title*[tit::title]\<open>My Personal, Ecclectic Isabelle Programming Manual\<close>
subtitle*[stit::subtitle]\<open>Version : Isabelle 2019\<close>
subtitle*[stit::subtitle]\<open>Version : Isabelle 2020\<close>
text*[bu::author,
email = "''wolff@lri.fr''",
affiliation = "\<open>Université Paris-Saclay, LRI, France\<close>"]\<open>Burkhart Wolff\<close>

2
src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty
View File

@ -14,7 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-cenelec_50128}
[2019/08/18 Unreleased/Isabelle2019%
[2019/08/18 Unreleased/Isabelle2020%
Document-Type Support Framework for Isabelle (CENELEC 50128).]
\RequirePackage{DOF-COL}

2
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -14,7 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper}
[2020/01/14 Unreleased/Isabelle2019%
[2020/01/14 Unreleased/Isabelle2020%
Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{DOF-COL}