nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

doc updates and layout in Refman.

This commit is contained in:
Burkhart Wolff 2022-02-24 22:01:52 +01:00
parent 51b3e74c36
commit 913bf49b3f
3 changed files with 18 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -119,10 +119,17 @@ text\<open>
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019. Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
\href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}. \href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
\end{quote} \end{quote}
A \<^BibTeX>-entry is available at: A \<^BibTeX>-entry is available at:
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>. \<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
\<^item> for an application of \<^isadof> in the context of certifications:
\begin{quote}\small
A.~D. Brucker and B.~Wolff.
Using Ontologies in Formal Developments Targeting Certification.
In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
\href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
\end{quote}
\<close> \<close>
subsubsection\<open>Availability\<close> subsubsection\<open>Availability\<close>
text\<open> text\<open>

6
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -43,11 +43,11 @@ The current system framework offers moreover the following features:
\<^item> an extensible front-end language Isabelle/Isar, and, \<^item> an extensible front-end language Isabelle/Isar, and,
\<^item> last but not least, an LCF style, generic theorem prover kernel as \<^item> last but not least, an LCF style, generic theorem prover kernel as
the most prominent and deeply integrated system component. the most prominent and deeply integrated system component.
\<close>
text\<open>
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>. 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 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>. 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

12
examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
View File

@ -41,8 +41,8 @@
\pagestyle{headings} \pagestyle{headings}
\uppertitleback{ \uppertitleback{
Copyright \copyright{} 2019--2021 University of Exeter, UK\\ Copyright \copyright{} 2019--2022 University of Exeter, UK\\
\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\ \phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
\phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\ \phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
\smallskip \smallskip
@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
\lowertitleback{% \lowertitleback{%
This manual describes \isadof version \isadofversion. The latest official This manual describes \isadof version \isadofversion. The latest official
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release. The latest development version as well as official releases are available at release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}).
The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest
release. The latest development version as well as official releases are available at
\url{\dofurl}. \url{\dofurl}.
\paragraph*{Contributors.} We would like to thank the following contributors to \isadof \paragraph*{Contributors.} We would like to thank the following contributors to \isadof
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric. (in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, \paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay,
France, and therefore granted with public funds of the Program ``Investissements d'Avenir.'' France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
\hfill \hfill
\begin{minipage}{8cm} \begin{minipage}{8cm}
\raggedleft\normalsize \raggedleft\normalsize
Laboratoire en Recherche en Informatique (LRI)\\ Laboratoire des Methodes Formelles (LMF)\\
Universit\'e Paris-Saclay\\ Universit\'e Paris-Saclay\\
91405 Orsay Cedex\\ 91405 Orsay Cedex\\
France France