forked from Isabelle_DOF/Isabelle_DOF
Make 2021-ITP-PMTI paper compile
This commit is contained in:
Nicolas Méric
parent
96112ff893
commit
688e823463
|
|
@ -15,3 +15,4 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" +
|
|||
"figures/three-phase-odo.pdf"
|
||||
"figures/df-numerics-encshaft.png"
|
||||
"figures/wheel-df.png"
|
||||
"lstisadof.sty"
|
||||
|
|
|
|||
|
|
@ -0,0 +1,163 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Saclay
|
||||
%% 2019 The University of Exeter
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1.3c of the License, or (at your option) any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
|
||||
|
||||
\definecolor{OliveGreen} {cmyk}{0.64,0,0.95,0.40}
|
||||
\definecolor{BrickRed} {cmyk}{0,0.89,0.94,0.28}
|
||||
\definecolor{Blue} {cmyk}{1,1,0,0}
|
||||
\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
|
||||
|
||||
%%%\lst@BeginAspect[keywords]{isar}
|
||||
\gdef\lst@tagtypes{s}
|
||||
\gdef\lst@TagKey#1#2{%
|
||||
\lst@Delim\lst@tagstyle #2\relax
|
||||
{Tag}\lst@tagtypes #1%
|
||||
{\lst@BeginTag\lst@EndTag}%
|
||||
\@@end\@empty{}}
|
||||
\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
|
||||
\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
|
||||
\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
|
||||
\gdef\lst@BeginTag{%
|
||||
\lst@DelimOpen
|
||||
\lst@ifextags\else
|
||||
{\let\lst@ifkeywords\iftrue
|
||||
\lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
|
||||
\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
|
||||
\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
|
||||
\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
|
||||
\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
|
||||
\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
|
||||
\global\let\lst@iffirstintag\iffalse
|
||||
\lst@AddToHook{PostOutput}{\lst@tagresetfirst}
|
||||
\lst@AddToHook{Output}
|
||||
{\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
|
||||
\lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
|
||||
\lst@AddToHook{Output}
|
||||
{\ifnum\lst@mode=\lst@tagmode
|
||||
\lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
|
||||
\lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
|
||||
\fi}
|
||||
\lst@NewMode\lst@tagmode
|
||||
\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
|
||||
\lst@CArg #1\relax\lst@DefDelimB {}{}%
|
||||
{\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
|
||||
#3\lst@tagmode{#5}%
|
||||
\lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
|
||||
\gdef\lst@BeginCDATA#1\@empty{%
|
||||
\lst@TrackNewLines \lst@PrintToken
|
||||
\lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
|
||||
\lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
|
||||
%%\lst@EndAspect
|
||||
|
||||
|
||||
|
||||
% \gdef\lst@BeginTag{%
|
||||
% \lst@DelimOpen
|
||||
% \lst@ifextags\else
|
||||
% {\let\lst@ifkeywords\iftrue
|
||||
% \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}}
|
||||
% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}}
|
||||
|
||||
\def\beginlstdelim#1#2#3%
|
||||
{%
|
||||
\def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
|
||||
\ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
|
||||
}
|
||||
\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
|
||||
\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
|
||||
\lstdefinestyle{ISAR}{%
|
||||
language=%
|
||||
,basicstyle=\ttfamily%
|
||||
,showspaces=false%
|
||||
,showlines=false%
|
||||
,columns=flexible%
|
||||
,morecomment=[s]{(*}{*)}%
|
||||
% ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
|
||||
,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
|
||||
,showstringspaces=false%
|
||||
,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
|
||||
,literate={%
|
||||
{...}{\,\ldots\,}3%
|
||||
{\\<Open>}{\ensuremath{\isacartoucheopen}}1%
|
||||
{\\at}{@}1%
|
||||
{\\<Close>}{\ensuremath{\isacartoucheclose}}1%
|
||||
{\\<Gamma>}{\ensuremath{\Gamma}}1%
|
||||
{\\<times>}{\ensuremath{\times}}1%
|
||||
{\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
|
||||
{\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
|
||||
{\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
|
||||
{\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
|
||||
{\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
|
||||
{\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
|
||||
{*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
|
||||
}%
|
||||
% % Defining "tags" (text-antiquotations) based on 1-keywords
|
||||
,tag=**[s]{@\{}{\}}%
|
||||
,tagstyle=\color{CornflowerBlue}%
|
||||
,markfirstintag=true%
|
||||
,keywordstyle=\bfseries%
|
||||
,keywords={}
|
||||
% Defining 2-keywords
|
||||
,keywordstyle=[2]{\color{Blue!60}\bfseries}%
|
||||
,alsoletter={*,-}
|
||||
,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
|
||||
%,moredelim=[s][\textit]{<}{>}
|
||||
% Defining 3-keywords
|
||||
,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
|
||||
,morekeywords=[3]{doc_class,declare_reference,update_instance*,
|
||||
open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}%
|
||||
% Defining 4-keywords
|
||||
,keywordstyle=[4]{\color{black!60}\bfseries}%
|
||||
,morekeywords=[4]{where, imports}%
|
||||
% Defining 5-keywords
|
||||
,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
|
||||
,morekeywords=[5]{datatype, typedecl, consts, theorem}%
|
||||
% Defining 6-keywords
|
||||
,keywordstyle=[6]{\itshape}%
|
||||
,morekeywords=[6]{meta-args, ref, expr, class_id}%
|
||||
%
|
||||
}%
|
||||
%%
|
||||
\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
|
||||
backgroundcolor=\color{black!2},
|
||||
frame=lines,
|
||||
mathescape=true,
|
||||
basicstyle=\footnotesize\ttfamily,#1}}{}
|
||||
%%%
|
||||
\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
|
||||
|
||||
\lstnewenvironment{out}[1][]{\lstset{
|
||||
backgroundcolor=\color{green!2},
|
||||
frame=lines,mathescape,breakatwhitespace=true
|
||||
,columns=flexible%
|
||||
,basicstyle=\footnotesize\rmfamily,#1}}{}
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%
|
||||
%%%%%%%%%%%%%%%%%%
|
||||
\lstloadlanguages{ML}
|
||||
\lstdefinestyle{sml}{basicstyle=\ttfamily,%
|
||||
commentstyle=\itshape,%
|
||||
keywordstyle=\bfseries\color{CornflowerBlue},%
|
||||
ndkeywordstyle=\color{red},%
|
||||
language=ML,
|
||||
,keywordstyle=[6]{\itshape}%
|
||||
,morekeywords=[6]{args_type}%
|
||||
}%
|
||||
|
||||
\lstnewenvironment{sml}[1][]{\lstset{style=sml,
|
||||
backgroundcolor=\color{Blue!4},
|
||||
frame=lines,
|
||||
basicstyle=\footnotesize\ttfamily,#1}}{}
|
||||
%%%
|
||||
\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
|
||||
|
|
@ -1,10 +1,16 @@
|
|||
%% This is a placeholder for user-specific configuration and packages.
|
||||
%% This is a placeholder for user-specific configuration and packages.
|
||||
|
||||
\usepackage{stmaryrd}
|
||||
\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}%
|
||||
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}%
|
||||
\usepackage{textcomp}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{paralist}
|
||||
\usepackage{listings}
|
||||
\usepackage{lstisadof}
|
||||
\usepackage{xspace}
|
||||
|
||||
\newcommand{\acs}[1]{}
|
||||
\newcommand{\fixIsarList}{\vspace{-\topsep}\vspace{-\baselineskip}\mbox{}\\[0pt]\noindent}
|
||||
|
||||
\title{<TITLE>}
|
||||
\author{<AUTHOR>}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -13,6 +13,132 @@
|
|||
@STRING{j-tosem= "" }
|
||||
@STRING{pub-acm:adr= "" }
|
||||
|
||||
@TechReport{ bsi:50128:2014,
|
||||
type = {Standard},
|
||||
key = {BS EN 50128:2011},
|
||||
month = apr,
|
||||
year = 2014,
|
||||
series = {British Standards Publication},
|
||||
title = {BS EN 50128:2011: Railway applications -- Communication,
|
||||
signalling and processing systems -- Software for railway
|
||||
control and protecting systems},
|
||||
institution = {Britisch Standards Institute (BSI)},
|
||||
keywords = {CENELEC},
|
||||
abstract = {This European Standard is part of a group of related
|
||||
standards. The others are EN 50126-1:1999 "Railway
|
||||
applications -- The specification and demonstration of
|
||||
Reliability, Availability, Maintainability and Safety
|
||||
(RAMS) -- Part 1: Basic requirements and generic process --
|
||||
and EN 50129:2003 "Railway applications -- Communication,
|
||||
signalling and processing systems -- Safety related
|
||||
electronic systems for signalling". EN 50126-1 addresses
|
||||
system issues on the widest scale, while EN 50129 addresses
|
||||
the approval process for individual systems which can exist
|
||||
within the overall railway control and protection system.
|
||||
This European Standard concentrates on the methods which
|
||||
need to be used in order to provide software which meets
|
||||
the demands for safety integrity which are placed upon it
|
||||
by these wider considerations. This European Standard
|
||||
provides a set of requirements with which the development,
|
||||
deployment and maintenance of any safety-related software
|
||||
intended for railway control and protection applications
|
||||
shall comply. It defines requirements concerning
|
||||
organisational structure, the relationship between
|
||||
organisations and division of responsibility involved in
|
||||
the development, deployment and maintenanceactivities.}
|
||||
}
|
||||
|
||||
@InCollection{ brucker.ea:isabelledof:2019,
|
||||
abstract = {DOF is a novel framework for defining ontologies and
|
||||
enforcing them during document development and evolution. A
|
||||
major goal of DOF is the integrated development of formal
|
||||
certification documents (e. g., for Common Criteria or
|
||||
CENELEC 50128) that require consistency across both formal
|
||||
and informal arguments.
|
||||
|
||||
To support a consistent development of formal and informal
|
||||
parts of a document, we provide Isabelle/DOF, an
|
||||
implementation of DOF on top of the formal methods
|
||||
framework Isabelle/HOL. A particular emphasis is put on a
|
||||
deep integration into Isabelle{\^a}s IDE, which allows for
|
||||
smooth ontology development as well as immediate
|
||||
ontological feedback during the editing of a document.
|
||||
|
||||
In this paper, we give an in-depth presentation of the
|
||||
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
|
||||
informal parts in an LCF-style interactive theorem proving
|
||||
environment. Sufficiently annotated, large documents can
|
||||
easily be developed collabo- ratively, while ensuring their
|
||||
consistency, and the impact of changes (in the formal and
|
||||
the semi-formal content) is tracked automatically.},
|
||||
keywords = {Ontology, Formal Document Development, CERtification, DOF,
|
||||
Isabelle/DOF},
|
||||
location = {Oslo},
|
||||
author = {Achim D. Brucker and Burkhart Wolff},
|
||||
booktitle = {Software Engineering and Formal Methods (SEFM)},
|
||||
language = {USenglish},
|
||||
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Heidelberg},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
number = {11724},
|
||||
isbn = {3-540-25109-X},
|
||||
doi = {10.1007/978-3-030-30446-1_15},
|
||||
editor = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n},
|
||||
pdf = {https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf},
|
||||
title = {{Isabelle/DOF}: Design and Implementation},
|
||||
classification= {conference},
|
||||
areas = {formal methods, software},
|
||||
categories = {isadof},
|
||||
year = {2019},
|
||||
public = {yes}
|
||||
}
|
||||
|
||||
@InCollection{ brucker.ea:isabelle-ontologies:2018,
|
||||
abstract = {While Isabelle is mostly known as part of Isabelle/HOL (an
|
||||
interactive theorem prover), it actually provides a
|
||||
framework for developing a wide spectrum of applications. A
|
||||
particular strength of the Isabelle framework is the
|
||||
combination of text editing, formal verification, and code
|
||||
generation.
|
||||
|
||||
Up to now, Isabelle's document preparation system lacks a
|
||||
mechanism for ensuring the structure of different document
|
||||
types (as, e.g., required in certification processes) in
|
||||
general and, in particular, mechanism for linking informal
|
||||
and formal parts of a document.
|
||||
|
||||
In this paper, we present Isabelle/DOF, a novel Document
|
||||
Ontology Framework on top of Isabelle. Isabelle/DOF allows
|
||||
for conventional typesetting \emph{as well} as formal
|
||||
development. We show how to model document ontologies
|
||||
inside Isabelle/DOF, how to use the resulting
|
||||
meta-information for enforcing a certain document
|
||||
structure, and discuss ontology-specific IDE support.},
|
||||
keywords = {Isabelle/Isar, HOL, Ontologies},
|
||||
location = {Hagenberg, Austria},
|
||||
author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli
|
||||
and Burkhart Wolff},
|
||||
booktitle = {Conference on Intelligent Computer Mathematics (CICM)},
|
||||
language = {USenglish},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Heidelberg},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
number = {11006},
|
||||
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018},
|
||||
title = {Using the {Isabelle} Ontology Framework: Linking the
|
||||
Formal with the Informal},
|
||||
classification= {conference},
|
||||
areas = {formal methods, software},
|
||||
categories = {isadof},
|
||||
public = {yes},
|
||||
year = {2018},
|
||||
doi = {10.1007/978-3-319-96812-4_3},
|
||||
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf}
|
||||
}
|
||||
|
||||
% $Id: fmde.bib 6539 2010-01-29 10:33:20Z brucker $
|
||||
|
||||
|
|
@ -4424,34 +4550,34 @@ isbn="978-3-540-48509-4"
|
|||
maiden name is Diana Senn.}
|
||||
}
|
||||
|
||||
@InCollection{ wenzel.ea:building:2007,
|
||||
abstract = {We present the generic system framework of
|
||||
Isabelle/Isarunderlying recent versions of Isabelle. Among
|
||||
other things, Isar provides an infrastructure for Isabelle
|
||||
plug-ins, comprising extensible state components and
|
||||
extensible syntax that can be bound to tactical ML
|
||||
programs. Thus the Isabelle/Isar architecture may be
|
||||
understood as an extension and refinement of the
|
||||
traditional LCF approach, with explicit infrastructure for
|
||||
building derivative systems. To demonstrate the technical
|
||||
potential of the framework, we apply it to a concrete
|
||||
formalmethods tool: the HOL-Z 3.0 environment, which is
|
||||
geared towards the analysis of Z specifications and formal
|
||||
proof of forward-refinements.},
|
||||
author = {Makarius Wenzel and Burkhart Wolff},
|
||||
booktitle = {\acs{tphols} 2007},
|
||||
editor = {Klaus Schneider and Jens Brandt},
|
||||
language = {USenglish},
|
||||
@InCollection{ wenzel.ea:building:2007,
|
||||
abstract = {We present the generic system framework of
|
||||
Isabelle/Isarunderlying recent versions of Isabelle. Among
|
||||
other things, Isar provides an infrastructure for Isabelle
|
||||
plug-ins, comprising extensible state components and
|
||||
extensible syntax that can be bound to tactical ML
|
||||
programs. Thus the Isabelle/Isar architecture may be
|
||||
understood as an extension and refinement of the
|
||||
traditional LCF approach, with explicit infrastructure for
|
||||
building derivative systems. To demonstrate the technical
|
||||
potential of the framework, we apply it to a concrete
|
||||
formalmethods tool: the HOL-Z 3.0 environment, which is
|
||||
geared towards the analysis of Z specifications and formal
|
||||
proof of forward-refinements.},
|
||||
author = {Makarius Wenzel and Burkhart Wolff},
|
||||
booktitle = {TPHOLs 2007},
|
||||
editor = {Klaus Schneider and Jens Brandt},
|
||||
language = {USenglish},
|
||||
acknowledgement={none},
|
||||
pages = {352--367},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
number = 4732,
|
||||
series = s-lncs,
|
||||
title = {Building Formal Method Tools in the {Isabelle}/{Isar}
|
||||
Framework},
|
||||
doi = {10.1007/978-3-540-74591-4_26},
|
||||
year = 2007
|
||||
pages = {352--367},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
number = 4732,
|
||||
series = s-lncs,
|
||||
title = {Building Formal Method Tools in the {Isabelle}/{Isar}
|
||||
Framework},
|
||||
doi = {10.1007/978-3-540-74591-4_26},
|
||||
year = 2007
|
||||
}
|
||||
|
||||
@Article{ igarashi.ea:featherweight:2001,
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ author*[bu,email="\<open>wolff@lri.fr\<close>",affiliation = "\<open>LRI, Univer
|
|||
|
||||
abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\<close>,\<open>Formal Development\<close>,\<open>Isabelle/HOL\<close>,\<open>Ontology Alignment\<close>,\<open>OWL\<close>,\<open>UML/OCL\<close>]"]
|
||||
\<open> \<^dof> is a novel ontology framework on top of Isabelle
|
||||
@{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"}.
|
||||
@{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"}.
|
||||
\<^dof> allows for the formal development of ontologies as well as continuous checking that
|
||||
a formal document under development conforms to an underlying ontology.
|
||||
Such a document may contain text and code elements as well as formal Isabelle definitions and proofs.
|
||||
|
|
@ -43,6 +43,7 @@ abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\<
|
|||
content \<^bold>\<open>as well as\<close> formal proofs that establish relations between different ontologies in general
|
||||
and specific ontology instances in concrete cases. This concept is also called
|
||||
\<^emph>\<open>ontology alignment\<close> in the literature raised a substantial interest recently.
|
||||
% Verify papers ontology alignment
|
||||
\<close>
|
||||
|
||||
section*[introheader::introduction,main_author="Some(@{author ''bu''})"]
|
||||
|
|
@ -96,7 +97,7 @@ in the code-elements of Isabelle's SML implementation, or were specifically supp
|
|||
C-program contexts in Isabelle/C @{cite "Tuong-IsabelleC:2019"}.
|
||||
|
||||
However, programming antiquotations on the intern Isabelle API's is nothing for the
|
||||
faint-hearted. Recently, \<^dof> @{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"}
|
||||
faint-hearted. Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"}
|
||||
has been designed as an Isabelle component that \<^emph>\<open>generates\<close> antiquotation languages
|
||||
from a more abstract description, namely an \<^emph>\<open>ontology\<close> that provides typed meta-data
|
||||
and typed reference mechanisms inside text- and ML-contexts.
|
||||
|
|
@ -148,8 +149,7 @@ text\<open>
|
|||
subsection*[bgrnd_isadof::text_section]\<open>The \<^dof> Framework\<close>
|
||||
text\<open>
|
||||
\<^dof> ~@{cite "brucker.ea:isabelle-ontologies:2018" and
|
||||
"brucker.ea:isabelledof:2019" and
|
||||
"brucker.ea:isabelledof-sw"}
|
||||
"brucker.ea:isabelledof:2019"}
|
||||
is a document ontology framework that extends Isabelle/HOL. We understand
|
||||
by a \<^emph>\<open>document ontology\<close> structured meta-data attached to an integrated document allowing
|
||||
classifying text-elements, connect them to typed meta-data, and establishing typed links between text-
|
||||
|
|
@ -215,7 +215,7 @@ text\<open>
|
|||
ontology definition. Isabelle's session management allows for pre-compiling them before being
|
||||
imported in the actual target documentation required to be compliant to this ontology.
|
||||
|
||||
\vspace{-0.7cm}\<close>
|
||||
%\vspace{-0.7cm}\<close>
|
||||
|
||||
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Req-Def-ex''",
|
||||
caption="''A Text-Element as Requirement.''",relative_width="48",
|
||||
|
|
|
|||
Reference in New Issue