Merge branch 'main' into ICFEM-2022
20
etc/options
|
@ -2,7 +2,25 @@
|
|||
|
||||
section "Isabelle/DOF"
|
||||
|
||||
public option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
||||
public option dof_document_class : string = "scrreprt-modern"
|
||||
-- "Default document class for Isabelle/DOF documents"
|
||||
|
||||
public option dof_presentation_ontologies : string = "technical_report scholarly_paper"
|
||||
-- "ontologies (separated by blanks)"
|
||||
|
||||
|
||||
option dof_version : string = "Unreleased"
|
||||
-- "Isabelle/DOF version"
|
||||
(* "Unreleased" for development, semantic version for releases *)
|
||||
|
||||
option dof_isabelle : string = "2021-1"
|
||||
|
||||
option dof_latest_version : string = "1.2.0"
|
||||
option dof_latest_isabelle : string = "Isabelle2021"
|
||||
option dof_latest_doi : string = "10.5281/zenodo.6385695"
|
||||
option dof_generic_doi : string = "10.5281/zenodo.3370482"
|
||||
|
||||
option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
||||
-- "Isabelle/DOF source repository"
|
||||
|
||||
option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF"
|
||||
|
|
0
examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png
Executable file → Normal file
Before Width: | Height: | Size: 27 KiB After Width: | Height: | Size: 27 KiB |
Before Width: | Height: | Size: 407 KiB After Width: | Height: | Size: 407 KiB |
0
examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 23 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
Executable file → Normal file
|
@ -6,8 +6,10 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
|
|||
document_files
|
||||
"isadof.cfg"
|
||||
"root.bib"
|
||||
"authorarchive.sty"
|
||||
"preamble.tex"
|
||||
"lstisadof.sty"
|
||||
"vector_iD_icon.pdf"
|
||||
"figures/isabelle-architecture.pdf"
|
||||
"figures/Dogfood-Intro.png"
|
||||
"figures/InteractiveMathSheet.png"
|
||||
|
|
|
@ -0,0 +1,339 @@
|
|||
%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
|
||||
%%
|
||||
%% 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
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{authorarchive}
|
||||
[0000/00/00 Unreleased v1.1.1+%
|
||||
Self-archiving information for scientific publications.]
|
||||
%
|
||||
\PassOptionsToPackage{hyphens}{url}
|
||||
%
|
||||
\RequirePackage{ifthen}
|
||||
\RequirePackage[inline]{enumitem}
|
||||
\RequirePackage{graphicx}
|
||||
\RequirePackage{eso-pic}
|
||||
\RequirePackage{intopdf}
|
||||
\RequirePackage{kvoptions}
|
||||
\RequirePackage{hyperref}
|
||||
\RequirePackage{calc}
|
||||
\RequirePackage{qrcode}
|
||||
\RequirePackage{hvlogos}
|
||||
%
|
||||
%Better url breaking
|
||||
\g@addto@macro{\UrlBreaks}{\UrlOrds}
|
||||
%
|
||||
% Option declarations
|
||||
% -------------------
|
||||
\SetupKeyvalOptions{
|
||||
family=AA,
|
||||
prefix=AA@
|
||||
}
|
||||
%
|
||||
\DeclareStringOption[.]{bibtexdir}
|
||||
\DeclareStringOption[https://duckduckgo.com/?q=]{baseurl}
|
||||
\DeclareStringOption[.pdf]{suffix}
|
||||
\DeclareStringOption[UNKNOWN PUBLISHER]{publisher}[]
|
||||
\DeclareStringOption[UNKNOWN YEAR]{year}[]
|
||||
\DeclareStringOption[]{key}[]
|
||||
\DeclareStringOption[]{doi}[]
|
||||
\DeclareStringOption[]{doiText}[]
|
||||
\DeclareStringOption[]{publisherurl}[]
|
||||
\DeclareStringOption[UNKNOWN START PAGE]{startpage}[]
|
||||
\DeclareStringOption[UNKNOWN PUBLICATION]{publication}[]
|
||||
|
||||
\DeclareBoolOption{ACM}
|
||||
\DeclareBoolOption{acmart}
|
||||
\DeclareBoolOption{ENTCS}
|
||||
\DeclareBoolOption{IEEE}
|
||||
\DeclareBoolOption{LNCS}
|
||||
\DeclareBoolOption{LNI}
|
||||
\DeclareBoolOption{nocopyright}
|
||||
\DeclareBoolOption{nourl}
|
||||
\DeclareBoolOption{nobib}
|
||||
\DeclareBoolOption{orcidicon}
|
||||
%\ProcessOptions\relax
|
||||
|
||||
|
||||
% Default option rule
|
||||
\DeclareDefaultOption{%
|
||||
\ifx\CurrentOptionValue\relax
|
||||
\PackageWarningNoLine{\@currname}{%
|
||||
Unknown option `\CurrentOption'\MessageBreak
|
||||
is passed to package `authorarchive'%
|
||||
}%
|
||||
% Pass the option to package color.
|
||||
% Again it is better to expand \CurrentOption.
|
||||
\expandafter\PassOptionsToPackage\expandafter{\CurrentOption}{color}%
|
||||
\else
|
||||
% Package color does not take options with values.
|
||||
% We provide the standard LaTeX error.
|
||||
\@unknownoptionerror
|
||||
\fi
|
||||
}
|
||||
\ProcessKeyvalOptions*
|
||||
|
||||
% Provide command for dynamic configuration seutp
|
||||
\def\authorsetup{\kvsetkeys{AA}}
|
||||
|
||||
% Load local configuration
|
||||
\InputIfFileExists{authorarchive.config}{}{}
|
||||
|
||||
|
||||
\newlength\AA@x
|
||||
\newlength\AA@y
|
||||
\newlength\AA@width
|
||||
|
||||
\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
|
||||
\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
|
||||
\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
|
||||
\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
|
||||
\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
|
||||
|
||||
\newboolean{AA@bibExists}
|
||||
\setboolean{AA@bibExists}{false}
|
||||
\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
|
||||
\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
|
||||
\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
|
||||
\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
|
||||
\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
|
||||
|
||||
\setlength\AA@x{1in+\hoffset+\oddsidemargin}
|
||||
|
||||
\newcommand{\authorcrfont}{\footnotesize}
|
||||
\newcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{.2cm-\paperheight}){#1}}}
|
||||
\newcommand{\authorwidth}[1]{\setlength{\AA@width}{#1}}
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
|
||||
\def\AA@pageinfo{}
|
||||
\ifthenelse{\equal{\AA@startpage}{UNKNOWN START PAGE}}{%
|
||||
}{%
|
||||
\setcounter{page}{\AA@startpage}%
|
||||
\def\AA@pageinfo{pp. \thepage--\pageref{\aa@lastpage}, }
|
||||
}
|
||||
|
||||
|
||||
|
||||
%%%% sig-alternate.cls
|
||||
\ifAA@ACM%
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=ACM}
|
||||
}{}
|
||||
\global\boilerplate={}
|
||||
\global\copyrightetc={}
|
||||
\renewcommand{\conferenceinfo}[2]{}
|
||||
\renewcommand{\authorcrfont}{\scriptsize}
|
||||
\setlength\AA@x{1in+\hoffset+\oddsidemargin}
|
||||
\setlength\AA@y{-\textheight+\topmargin+\headheight-\footskip} % -\voffset-\topmargin-\headheight-\footskip}
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{\AA@y}){#1}}
|
||||
\setlength{\AA@width}{\columnwidth}
|
||||
\fi
|
||||
%
|
||||
%%%% acmart.cls
|
||||
\ifAA@acmart%
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=ACM}
|
||||
}{}
|
||||
\renewcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{0.2cm-\paperheight}){#1}}}
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
\fi
|
||||
%
|
||||
%%%% LNCS
|
||||
\ifAA@LNCS%
|
||||
\ifAA@orcidicon%
|
||||
\renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
|
||||
\textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
|
||||
\else\relax\fi%
|
||||
%
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=Springer-Verlag}
|
||||
}{}
|
||||
\renewcommand{\authorcrfont}{\scriptsize}
|
||||
\@ifclasswith{llncs}{a4paper}{%
|
||||
\ExplSyntaxOn
|
||||
\@ifundefined{pdfmanagement_add:nnn}{%
|
||||
\pdfpagesattr{/CropBox [92 114 523 780]}%
|
||||
}{%
|
||||
\pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
|
||||
}%
|
||||
\ExplSyntaxOff
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
|
||||
}{%
|
||||
\ExplSyntaxOn
|
||||
\@ifundefined{pdfmanagement_add:nnn}{%
|
||||
\pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
|
||||
}{%
|
||||
\pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
|
||||
}%
|
||||
\ExplSyntaxOff
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
|
||||
}
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
\setcounter{tocdepth}{2}
|
||||
\fi
|
||||
%
|
||||
%%%% LNI
|
||||
\ifAA@LNI%
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=GI}
|
||||
}{}
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
|
||||
\renewcommand{\authorcrfont}{\scriptsize}
|
||||
\pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
\setcounter{tocdepth}{2}
|
||||
\fi
|
||||
%
|
||||
%%%% ENTCS
|
||||
\ifAA@ENTCS%
|
||||
\addtolength{\voffset}{1cm}
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=Elsevier Science B.~V.}
|
||||
}{}
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{-.5cm-\the\ht\AA@authoratBox}){#1}}
|
||||
\renewcommand{\authorcrfont}{\scriptsize}
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
\fi
|
||||
%
|
||||
%%%% IEEE
|
||||
\ifAA@IEEE%
|
||||
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||
\setkeys{AA}{publisher=IEEE}
|
||||
}{}
|
||||
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},6){#1}}
|
||||
\renewcommand{\authorcrfont}{\scriptsize}
|
||||
\setlength{\AA@width}{\textwidth}
|
||||
\setcounter{tocdepth}{2}
|
||||
\fi
|
||||
%
|
||||
|
||||
\hypersetup{%
|
||||
draft = false,
|
||||
bookmarksopen = true,
|
||||
bookmarksnumbered= true,
|
||||
pdfauthor = {\@author},
|
||||
pdftitle = {\@title},
|
||||
}
|
||||
|
||||
\@ifpackageloaded{totpages}{%
|
||||
\def\aa@lastpage{TotPages}
|
||||
}{%
|
||||
\RequirePackage{lastpage}
|
||||
\def\aa@lastpage{LastPage}
|
||||
}
|
||||
\newsavebox{\AA@authoratBox}
|
||||
|
||||
\AddToShipoutPicture*{%
|
||||
\setlength{\unitlength}{1mm}%
|
||||
\savebox{\AA@authoratBox}{%
|
||||
\parbox{1.4cm}{%
|
||||
\bgroup%
|
||||
\normallineskiplimit=0pt%
|
||||
\ifAA@nourl%
|
||||
\ifx\AA@doi\@empty\relax%
|
||||
\else%
|
||||
\qrcode[hyperlink,height=1.17cm,padding]{https://doi.org/\AA@doi}%
|
||||
\fi%
|
||||
\else%
|
||||
\qrcode[hyperlink,height=1.17cm,padding]{\AA@baseurl/\AA@key\AA@suffix}%
|
||||
\fi%
|
||||
\egroup%
|
||||
}%
|
||||
\ifAA@nourl\ifx\AA@doi\@empty\addtolength{\AA@width}{1.4cm}\fi\fi
|
||||
\parbox{\AA@width-1.4cm}{\authorcrfont%
|
||||
\ifAA@LNCS%
|
||||
\AA@publication, \AA@pageinfo \AA@year. %
|
||||
\ifAA@nocopyright\else
|
||||
\textcopyright~\AA@year~\AA@publisher.
|
||||
\fi
|
||||
This is the author's
|
||||
version of the work. It is posted
|
||||
\ifAA@nourl\relax\else%
|
||||
at \url{\AA@baseurl/\AA@key\AA@suffix} %
|
||||
\fi
|
||||
\ifAA@nocopyright\relax\else
|
||||
by permission of \AA@publisher{}
|
||||
\fi
|
||||
for your personal use.
|
||||
\ifx\AA@doi\@empty%
|
||||
\relax
|
||||
\else
|
||||
The final publication is available at Springer via
|
||||
\ifx\AA@doiText\@empty%
|
||||
\url{https://doi.org/\AA@doi}.
|
||||
\else
|
||||
\href{https://doi.org/\AA@doi}{\AA@doiText}.
|
||||
\fi
|
||||
\fi
|
||||
\else
|
||||
\ifAA@nocopyright\relax\else
|
||||
\textcopyright~\AA@year~\AA@publisher. %
|
||||
\fi%
|
||||
This is the author's
|
||||
version of the work. It is posted
|
||||
\ifAA@nourl\relax\else%
|
||||
at \url{\AA@baseurl/\AA@key\AA@suffix} %
|
||||
\fi
|
||||
\ifAA@nocopyright\relax\else
|
||||
by permission of \AA@publisher{} %
|
||||
\fi
|
||||
for your personal use. Not for redistribution. The definitive
|
||||
version was published in \emph{\AA@publication}, \AA@pageinfo \AA@year%
|
||||
\ifx\AA@doi\@empty%
|
||||
\ifx\AA@publisherurl\@empty%
|
||||
.%
|
||||
\else
|
||||
\url{\AA@publisherurl}.%
|
||||
\fi
|
||||
\else
|
||||
\ifx\AA@doiText\@empty%
|
||||
, doi: \href{https://doi.org/\AA@doi}{\AA@doi}.%
|
||||
\else
|
||||
, doi: \href{https://doi.org/\AA@doi}{\AA@doiText}.%
|
||||
\fi
|
||||
\fi
|
||||
\fi
|
||||
\ifAA@nobib\relax\else%
|
||||
\ifthenelse{\boolean{AA@bibExists}}{%
|
||||
\hfill
|
||||
\begin{itemize*}[label={}, itemjoin={,}]
|
||||
\IfFileExists{\AA@bibBibTeX}{%
|
||||
\item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
|
||||
}{%
|
||||
\IfFileExists{\AA@bibBibTeXLong}{%
|
||||
\item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
|
||||
}{%
|
||||
\typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
|
||||
}%
|
||||
}%
|
||||
\IfFileExists{\AA@bibWord}{%
|
||||
\item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
|
||||
}{%
|
||||
\typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
|
||||
}%
|
||||
\IfFileExists{\AA@bibEndnote}{%
|
||||
\item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
|
||||
}{%
|
||||
\typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
|
||||
}%
|
||||
\IfFileExists{\AA@bibRIS}{%
|
||||
\item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
|
||||
}{%
|
||||
\typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
|
||||
}%
|
||||
\end{itemize*}\\
|
||||
}{%
|
||||
\PackageError{authorarchive}{No bibliographic files found. Specify option 'nobib' if this is intended.}
|
||||
}
|
||||
\fi
|
||||
}
|
||||
}
|
||||
\authorat{\raisebox{\the\ht\AA@authoratBox}{\usebox{\AA@authoratBox}}}
|
||||
}
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png
Executable file → Normal file
Before Width: | Height: | Size: 14 KiB After Width: | Height: | Size: 14 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 23 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png
Executable file → Normal file
Before Width: | Height: | Size: 85 KiB After Width: | Height: | Size: 85 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png
Executable file → Normal file
Before Width: | Height: | Size: 16 KiB After Width: | Height: | Size: 16 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png
Executable file → Normal file
Before Width: | Height: | Size: 75 KiB After Width: | Height: | Size: 75 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png
Executable file → Normal file
Before Width: | Height: | Size: 96 KiB After Width: | Height: | Size: 96 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg
Executable file → Normal file
Before Width: | Height: | Size: 57 KiB After Width: | Height: | Size: 57 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png
Executable file → Normal file
Before Width: | Height: | Size: 67 KiB After Width: | Height: | Size: 67 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png
Executable file → Normal file
Before Width: | Height: | Size: 50 KiB After Width: | Height: | Size: 50 KiB |
2
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg
Executable file → Normal file
|
@ -1,2 +1,2 @@
|
|||
Template: scrartcl
|
||||
Template: lncs
|
||||
Ontology: scholarly_paper
|
||||
|
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty
Executable file → Normal file
29
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex
Executable file → Normal file
|
@ -53,23 +53,18 @@
|
|||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
|
||||
\subject{Example of an Academic Paper\footnote{%
|
||||
This document is an example setup for writing an academic paper. While
|
||||
it is optimized for the Springer's LNCS class, it uses a Koma Script
|
||||
LaTeX class to avoid the re-distribution of \texttt{llncs.cls},
|
||||
which would violate Springer's copyright. This example has been
|
||||
published at CICM 2018:
|
||||
\protect\begin{quote}
|
||||
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and
|
||||
Burkhart Wolff. Using The Isabelle Ontology Framework: Linking
|
||||
the Formal with the Informal. In Conference on Intelligent
|
||||
Computer Mathematics (CICM). Lecture Notes in Computer Science
|
||||
(11006), Springer-Verlag, 2018.
|
||||
\protect\end{quote}
|
||||
Note that the content of this example is not updated and, hence,
|
||||
might not be correct with respect to the latest version of
|
||||
\isadof{}.
|
||||
}}
|
||||
\usepackage[LNCS,
|
||||
orcidicon,
|
||||
key=brucker.ea-isabelle-ontologies-2018,
|
||||
year=2018,
|
||||
publication={F. Rabe et al. (Eds.): CICM 2018, LNAI 11006},
|
||||
nobib,
|
||||
startpage={1},
|
||||
doi={10.1007/978-3-319-96812-4_3},
|
||||
doiText={10.1007/978-3-319-96812-4\_3},
|
||||
]{authorarchive}
|
||||
\authorrunning{A. D. Brucker et al.}
|
||||
\pagestyle{headings}
|
||||
|
||||
|
||||
\title{<TITLE>}
|
||||
|
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib
Executable file → Normal file
|
@ -181,7 +181,6 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
|||
-o ONTOLOGY (default: scholarly_paper)
|
||||
Available ontologies:
|
||||
* CENELEC_50128
|
||||
* math_exam
|
||||
* scholarly_paper
|
||||
* technical_report
|
||||
-t TEMPLATE (default: scrartcl)
|
||||
|
@ -505,9 +504,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
|
|||
caption2="''Exploring an attribute (hyperlinked to the class).''",
|
||||
relative_width2="47",
|
||||
src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
|
||||
(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
|
||||
to align them. This has to wait that the exploration of an attribute is again possible.
|
||||
See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
|
||||
|
||||
text\<open>
|
||||
From these class definitions, \<^isadof> also automatically generated editing
|
||||
|
|
|
@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel.
|
|||
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
|
||||
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
|
@ -1009,9 +1009,6 @@ text\<open>
|
|||
these types. They are just types declared in HOL,
|
||||
which are ``inhabited'' by special constant symbols carrying strings, for
|
||||
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
|
||||
% TODO:
|
||||
% Update meta-types implementation explanation to the new implementation
|
||||
% in repository commit 08c101c5440eee2a087068581952026e88c39f6a
|
||||
When HOL
|
||||
expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
|
||||
instance attributes, this requires additional checks after
|
||||
|
|
0
examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy
Executable file → Normal file
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png
Executable file → Normal file
Before Width: | Height: | Size: 14 KiB After Width: | Height: | Size: 10 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 10 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 17 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png
Executable file → Normal file
Before Width: | Height: | Size: 85 KiB After Width: | Height: | Size: 85 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png
Executable file → Normal file
Before Width: | Height: | Size: 16 KiB After Width: | Height: | Size: 13 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/MyCommentedIsabelle.png
Executable file → Normal file
Before Width: | Height: | Size: 162 KiB After Width: | Height: | Size: 162 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png
Executable file → Normal file
Before Width: | Height: | Size: 43 KiB After Width: | Height: | Size: 43 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png
Executable file → Normal file
Before Width: | Height: | Size: 214 KiB After Width: | Height: | Size: 214 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png
Executable file → Normal file
Before Width: | Height: | Size: 135 KiB After Width: | Height: | Size: 135 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 73 KiB After Width: | Height: | Size: 73 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/definition-use-CSP-pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 70 KiB After Width: | Height: | Size: 70 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg
Executable file → Normal file
Before Width: | Height: | Size: 36 KiB After Width: | Height: | Size: 36 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 203 KiB After Width: | Height: | Size: 203 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg
Executable file → Normal file
Before Width: | Height: | Size: 57 KiB After Width: | Height: | Size: 57 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png
Executable file → Normal file
Before Width: | Height: | Size: 81 KiB After Width: | Height: | Size: 81 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png
Executable file → Normal file
Before Width: | Height: | Size: 37 KiB After Width: | Height: | Size: 37 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png
Executable file → Normal file
Before Width: | Height: | Size: 26 KiB After Width: | Height: | Size: 26 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png
Executable file → Normal file
Before Width: | Height: | Size: 13 KiB After Width: | Height: | Size: 13 KiB |
0
examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf
Executable file → Normal file
Before Width: | Height: | Size: 91 KiB After Width: | Height: | Size: 91 KiB |
0
examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf
Executable file → Normal file
Before Width: | Height: | Size: 31 KiB After Width: | Height: | Size: 31 KiB |
0
examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/preamble.tex
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/root.bib
Executable file → Normal file
|
@ -1010,8 +1010,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
|
|||
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
||||
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
(base_name')
|
||||
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
(base_name' ^ " List.list")
|
||||
val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
|
||||
val table_list = Symtab.dest tab
|
||||
fun get_instances_name_list _ [] = []
|
||||
|
@ -1028,13 +1026,7 @@ fun elaborate_instances_list thy isa_name _ _ _ =
|
|||
end
|
||||
val long_class_name = DOF_core.read_cid_global thy base_name'
|
||||
val values_list = get_instances_name_list long_class_name table_list
|
||||
val hol_list_terms_list =
|
||||
fold
|
||||
(fn x =>
|
||||
fn y =>
|
||||
Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
|
||||
values_list (Const (@{const_name "Nil"}, class_list_typ))
|
||||
in hol_list_terms_list end
|
||||
in HOLogic.mk_list class_typ values_list end
|
||||
|
||||
fun declare_class_instances_annotation thy doc_class_name =
|
||||
let
|
||||
|
@ -1244,13 +1236,34 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init
|
|||
|
||||
fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
|
||||
(S:(string * Position.T * string * term)list) term =
|
||||
let val cid_ty = cid_2_cidType cid_long thy
|
||||
let val cid_ty = cid_2_cidType cid_long thy
|
||||
val generalize_term = Term.map_types (generalize_typ 0)
|
||||
fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t
|
||||
fun instantiate_term S t =
|
||||
Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t)
|
||||
fun read_assn (lhs, pos:Position.T, opr, rhs) term =
|
||||
let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
|
||||
let
|
||||
fun get_class_name parent_cid attribute_name pos =
|
||||
let
|
||||
val {attribute_decl, inherits_from, ...} =
|
||||
the (DOF_core.get_doc_class_global parent_cid thy)
|
||||
in
|
||||
if exists (fn (binding, _, _) => Binding.name_of binding = attribute_name)
|
||||
attribute_decl
|
||||
then parent_cid
|
||||
else
|
||||
case inherits_from of
|
||||
NONE =>
|
||||
ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos
|
||||
| SOME (_, parent_name) =>
|
||||
get_class_name parent_name attribute_name pos
|
||||
end
|
||||
val attr_defined_cid = get_class_name cid_long lhs pos
|
||||
val {id, name, ...} = the (DOF_core.get_doc_class_global attr_defined_cid thy)
|
||||
val markup = docclass_markup false cid_long id (Binding.pos_of name);
|
||||
val ctxt = Context.Theory thy
|
||||
val _ = Context_Position.report_generic ctxt pos markup;
|
||||
val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
|
||||
val (ln,lnt,lnu,lnut) = case info_opt of
|
||||
NONE => error ("unknown attribute >"
|
||||
^((Long_Name.base_name lhs))
|
||||
|
@ -1353,14 +1366,11 @@ fun check_invariants thy oid =
|
|||
let
|
||||
val value = the (DOF_core.get_value_global oid thy)
|
||||
val cid = #cid (the (DOF_core.get_object_global oid thy))
|
||||
(*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*)
|
||||
fun get_all_invariants cid thy =
|
||||
let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => error("undefined class id for invariants: " ^ cid)
|
||||
| SOME ({inherits_from=NONE, ...}) => invs
|
||||
| SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
|
||||
end
|
||||
case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => error("undefined class id for invariants: " ^ cid)
|
||||
| SOME ({inherits_from=NONE, invs, ...}) => invs
|
||||
| SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy)
|
||||
val invariants = get_all_invariants cid thy
|
||||
val inv_and_apply_list =
|
||||
let fun mk_inv_and_apply inv value thy =
|
||||
|
@ -2008,7 +2018,7 @@ fun print_doc_items b ctxt =
|
|||
writeln (" type: "^cid);
|
||||
case vcid of NONE => () | SOME (s) =>
|
||||
writeln (" virtual type: "^ s);
|
||||
writeln (" origine: "^thy_name);
|
||||
writeln (" origin: "^thy_name);
|
||||
writeln (" inline: "^dfg inline);
|
||||
writeln (" input_term: "
|
||||
^ (Syntax.string_of_term
|
||||
|
|
|
@ -7,8 +7,6 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
|||
"ontologies"
|
||||
"ontologies/CENELEC_50128"
|
||||
"ontologies/Conceptual"
|
||||
"ontologies/math_exam"
|
||||
"ontologies/math_paper"
|
||||
"ontologies/scholarly_paper"
|
||||
"ontologies/small_math"
|
||||
"ontologies/technical_report"
|
||||
|
|
|
@ -90,7 +90,7 @@ do
|
|||
NAME="$OPTARG"
|
||||
;;
|
||||
o)
|
||||
if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies/*//DOF-$OPTARG.sty" ]; then
|
||||
if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies"/*/DOF-$OPTARG.sty ]; then
|
||||
echo "ERROR: Ontology $OPTARG not available!"
|
||||
exit 1
|
||||
fi
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
\usepackage{isabellesym}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{DOF-amssymb}
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
\IfFileExists{DOF-core.sty}{}{%
|
||||
\PackageError{DOF-core}{Isabelle/DOF not installed.
|
||||
This is a Isabelle_DOF project. The document preparation requires
|
||||
|
@ -102,7 +101,7 @@
|
|||
{\small \renewcommand{\doi}[1]{}
|
||||
\newcommand{\urlprefix}{}
|
||||
|
||||
\bibliographystyle{spmpscinat}
|
||||
\bibliographystyle{splncs04}
|
||||
|
||||
\bibliography{root}
|
||||
}}{}
|
||||
|
|