diff --git a/CITATION b/CITATION old mode 100755 new mode 100644 diff --git a/LICENSE b/LICENSE old mode 100755 new mode 100644 diff --git a/README.md b/README.md old mode 100755 new mode 100644 diff --git a/ROOTS b/ROOTS old mode 100755 new mode 100644 diff --git a/etc/options b/etc/options index bd81e54..1e4ff4b 100644 --- a/etc/options +++ b/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" diff --git a/examples/CENELEC_50128/ROOTS b/examples/CENELEC_50128/ROOTS old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png b/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg b/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf b/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png b/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/isadof.cfg b/examples/CENELEC_50128/mini_odo/document/isadof.cfg old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/lstisadof.sty b/examples/CENELEC_50128/mini_odo/document/lstisadof.sty old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/preamble.tex b/examples/CENELEC_50128/mini_odo/document/preamble.tex old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/root.bib b/examples/CENELEC_50128/mini_odo/document/root.bib old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/document/root.mst b/examples/CENELEC_50128/mini_odo/document/root.mst old mode 100755 new mode 100644 diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy old mode 100755 new mode 100644 diff --git a/examples/README.md b/examples/README.md old mode 100755 new mode 100644 diff --git a/examples/ROOTS b/examples/ROOTS old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT old mode 100755 new mode 100644 index f50c278..bf79564 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT @@ -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" diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/authorarchive.sty b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/authorarchive.sty new file mode 100644 index 0000000..16328d3 --- /dev/null +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/authorarchive.sty @@ -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}}} +} diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg old mode 100755 new mode 100644 index dbf4a8e..19a8d78 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg @@ -1,2 +1,2 @@ -Template: scrartcl +Template: lncs Ontology: scholarly_paper diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex old mode 100755 new mode 100644 index b52751b..76965d0 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex @@ -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{} diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib old mode 100755 new mode 100644 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/vector_iD_icon.pdf b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/vector_iD_icon.pdf new file mode 100644 index 0000000..59824b1 Binary files /dev/null and b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/vector_iD_icon.pdf differ diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT index f585d67..da91e5b 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT +++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT @@ -1,13 +1,11 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = dof, - document_comment_latex = true] + options [document = pdf, document_output = "output", document_build = dof] theories "paper" document_files "isadof.cfg" "root.bib" "preamble.tex" - "spmpscinat.bst" "figures/Req-Appl-ex.png" "figures/formal-development.png" "figures/Req-Def-ex.png" diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/spmpscinat.bst b/examples/scholarly_paper/2021-ITP-PMTI/document/spmpscinat.bst deleted file mode 100644 index 7892349..0000000 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/spmpscinat.bst +++ /dev/null @@ -1,1588 +0,0 @@ -%% -%% NOTE: This BST file has been manually hacked to take comma out before -%% junior-part of names. See comments starting with "MANUAL:". -%% -%% NOTE: This BST file has been manually hacked to modify the FUNCTION -%% {begin.bib} in the following ways: -%% 1. Remove "\texttt" from "\url" definition -%% 2. Change "doi:" to "DOI~" in "\doi" definition with parameter -%% 3. Change "doi:" to "DOI~" in no-parameter "\doi" definition -%% See comments starting with "MANUAL:". -%% -%% This is file `spmpscinat.bst', -%% generated with the docstrip utility. -%% -%% The original source files were: -%% -%% merlin.mbs (with options: `vonx,nm-rvvc,yr-par,xmth,jttl-rm,thtit-a,vol-bf,volp-com,pgsep-c,num-xser,ser-vol,ser-ed,jnm-x,btit-rm,bt-rm,doi,edparxc,au-col,in-col,fin-bare,pp,ed,abr,xedn,jabr,xand,url,url-blk,nfss,ed-rev,pre-edn,ay,nat,etal-xc,jnrlab, ') -%% ---------------------------------------- -%% *** Intended for Journal of Mathematical Biology (with natbib support). *** -%% -%% Copyright 1994-2007 Patrick W Daly - % =============================================================== - % IMPORTANT NOTICE: - % This bibliographic style (bst) file has been generated from one or - % more master bibliographic style (mbs) files, listed above. - % - % This generated file 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 of the License, or any later version. - % =============================================================== - % Name and version information of the main mbs file: - % \ProvidesFile{merlin.mbs}[2007/04/24 4.20 (PWD, AO, DPC)] - % For use with BibTeX version 0.99a or later - %------------------------------------------------------------------- - % This bibliography style file is intended for texts in ENGLISH - % This is an author-year citation style bibliography. As such, it is - % non-standard LaTeX, and requires a special package file to function properly. - % Such a package is natbib.sty by Patrick W. Daly - % The form of the \bibitem entries is - % \bibitem[Jones et al.(1990)]{key}... - % \bibitem[Jones et al.(1990)Jones, Baker, and Smith]{key}... - % The essential feature is that the label (the part in brackets) consists - % of the author names, as they should appear in the citation, with the year - % in parentheses following. There must be no space before the opening - % parenthesis! - % With natbib v5.3, a full list of authors may also follow the year. - % In natbib.sty, it is possible to define the type of enclosures that is - % really wanted (brackets or parentheses), but in either case, there must - % be parentheses in the label. - % The \cite command functions as follows: - % \citet{key} ==>> Jones et al. (1990) - % \citet*{key} ==>> Jones, Baker, and Smith (1990) - % \citep{key} ==>> (Jones et al., 1990) - % \citep*{key} ==>> (Jones, Baker, and Smith, 1990) - % \citep[chap. 2]{key} ==>> (Jones et al., 1990, chap. 2) - % \citep[e.g.][]{key} ==>> (e.g. Jones et al., 1990) - % \citep[e.g.][p. 32]{key} ==>> (e.g. Jones et al., p. 32) - % \citeauthor{key} ==>> Jones et al. - % \citeauthor*{key} ==>> Jones, Baker, and Smith - % \citeyear{key} ==>> 1990 - %--------------------------------------------------------------------- - -ENTRY - { address - author - booktitle - chapter - doi - edition - editor - eid - howpublished - institution - journal - key - month - note - number - organization - pages - publisher - school - series - title - type - url - volume - year - } - {} - { label extra.label sort.label short.list } -INTEGERS { output.state before.all mid.sentence after.sentence after.block } -FUNCTION {init.state.consts} -{ #0 'before.all := - #1 'mid.sentence := - #2 'after.sentence := - #3 'after.block := -} -STRINGS { s t} -FUNCTION {output.nonnull} -{ 's := - output.state mid.sentence = - { ", " * write$ } - { output.state after.block = - { add.period$ write$ - newline$ - "\newblock " write$ - } - { output.state before.all = - 'write$ - { add.period$ " " * write$ } - if$ - } - if$ - mid.sentence 'output.state := - } - if$ - s -} -FUNCTION {output} -{ duplicate$ empty$ - 'pop$ - 'output.nonnull - if$ -} -FUNCTION {output.check} -{ 't := - duplicate$ empty$ - { pop$ "empty " t * " in " * cite$ * warning$ } - 'output.nonnull - if$ -} -FUNCTION {fin.entry} -{ duplicate$ empty$ - 'pop$ - 'write$ - if$ - newline$ -} - -FUNCTION {new.block} -{ output.state before.all = - 'skip$ - { after.block 'output.state := } - if$ -} -FUNCTION {new.sentence} -{ output.state after.block = - 'skip$ - { output.state before.all = - 'skip$ - { after.sentence 'output.state := } - if$ - } - if$ -} -FUNCTION {add.blank} -{ " " * before.all 'output.state := -} - -FUNCTION {add.colon} -{ duplicate$ empty$ - 'skip$ - { ":" * add.blank } - if$ -} - -FUNCTION {date.block} -{ - new.block -} - -FUNCTION {not} -{ { #0 } - { #1 } - if$ -} -FUNCTION {and} -{ 'skip$ - { pop$ #0 } - if$ -} -FUNCTION {or} -{ { pop$ #1 } - 'skip$ - if$ -} -FUNCTION {new.block.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.block - if$ -} -FUNCTION {field.or.null} -{ duplicate$ empty$ - { pop$ "" } - 'skip$ - if$ -} -FUNCTION {emphasize} -{ duplicate$ empty$ - { pop$ "" } - { "\emph{" swap$ * "}" * } - if$ -} -FUNCTION {bolden} -{ duplicate$ empty$ - { pop$ "" } - { "\textbf{" swap$ * "}" * } - if$ -} -FUNCTION {tie.or.space.prefix} -{ duplicate$ text.length$ #3 < - { "~" } - { " " } - if$ - swap$ -} - -FUNCTION {capitalize} -{ "u" change.case$ "t" change.case$ } - -FUNCTION {space.word} -{ " " swap$ * " " * } - % Here are the language-specific definitions for explicit words. - % Each function has a name bbl.xxx where xxx is the English word. - % The language selected here is ENGLISH -FUNCTION {bbl.and} -{ "and"} - -FUNCTION {bbl.etal} -{ "et~al." } - -FUNCTION {bbl.editors} -{ "eds." } - -FUNCTION {bbl.editor} -{ "ed." } - -FUNCTION {bbl.edby} -{ "edited by" } - -FUNCTION {bbl.edition} -{ "edn." } - -FUNCTION {bbl.volume} -{ "vol." } - -FUNCTION {bbl.of} -{ "of" } - -FUNCTION {bbl.number} -{ "no." } - -FUNCTION {bbl.nr} -{ "no." } - -FUNCTION {bbl.in} -{ "in" } - -FUNCTION {bbl.pages} -{ "pp." } - -FUNCTION {bbl.page} -{ "p." } - -FUNCTION {bbl.chapter} -{ "chap." } - -FUNCTION {bbl.techrep} -{ "Tech. Rep." } - -FUNCTION {bbl.mthesis} -{ "Master's thesis" } - -FUNCTION {bbl.phdthesis} -{ "Ph.D. thesis" } - -MACRO {jan} {"Jan."} - -MACRO {feb} {"Feb."} - -MACRO {mar} {"Mar."} - -MACRO {apr} {"Apr."} - -MACRO {may} {"May"} - -MACRO {jun} {"Jun."} - -MACRO {jul} {"Jul."} - -MACRO {aug} {"Aug."} - -MACRO {sep} {"Sep."} - -MACRO {oct} {"Oct."} - -MACRO {nov} {"Nov."} - -MACRO {dec} {"Dec."} - -MACRO {acmcs} {"ACM Comput. Surv."} - -MACRO {acta} {"Acta Inf."} - -MACRO {cacm} {"Commun. ACM"} - -MACRO {ibmjrd} {"IBM J. Res. Dev."} - -MACRO {ibmsj} {"IBM Syst.~J."} - -MACRO {ieeese} {"IEEE Trans. Software Eng."} - -MACRO {ieeetc} {"IEEE Trans. Comput."} - -MACRO {ieeetcad} - {"IEEE Trans. Comput. Aid. Des."} - -MACRO {ipl} {"Inf. Process. Lett."} - -MACRO {jacm} {"J.~ACM"} - -MACRO {jcss} {"J.~Comput. Syst. Sci."} - -MACRO {scp} {"Sci. Comput. Program."} - -MACRO {sicomp} {"SIAM J. Comput."} - -MACRO {tocs} {"ACM Trans. Comput. Syst."} - -MACRO {tods} {"ACM Trans. Database Syst."} - -MACRO {tog} {"ACM Trans. Graphic."} - -MACRO {toms} {"ACM Trans. Math. Software"} - -MACRO {toois} {"ACM Trans. Office Inf. Syst."} - -MACRO {toplas} {"ACM Trans. Progr. Lang. Syst."} - -MACRO {tcs} {"Theor. Comput. Sci."} - -FUNCTION {bibinfo.check} -{ swap$ - duplicate$ missing$ - { - pop$ pop$ - "" - } - { duplicate$ empty$ - { - swap$ pop$ - } - { swap$ - pop$ - } - if$ - } - if$ -} -FUNCTION {bibinfo.warn} -{ swap$ - duplicate$ missing$ - { - swap$ "missing " swap$ * " in " * cite$ * warning$ pop$ - "" - } - { duplicate$ empty$ - { - swap$ "empty " swap$ * " in " * cite$ * warning$ - } - { swap$ - pop$ - } - if$ - } - if$ -} -FUNCTION {format.url} -{ url empty$ - { "" } - { "\urlprefix\url{" url * "}" * } - if$ -} - -INTEGERS { nameptr namesleft numnames } - - -STRINGS { bibinfo} - -FUNCTION {format.names} -{ 'bibinfo := - duplicate$ empty$ 'skip$ { - 's := - "" 't := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr -% -% MANUAL: Removed comma before junior part. -% -% "{vv~}{ll}{, jj}{, f{.}.}" - "{vv~}{ll}{ jj}{, f{.}.}" - format.name$ - bibinfo bibinfo.check - 't := - nameptr #1 > - { - namesleft #1 > - { ", " * t * } - { - s nameptr "{ll}" format.name$ duplicate$ "others" = - { 't := } - { pop$ } - if$ - "," * - t "others" = - { - " " * bbl.etal * - } - { " " * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ - } if$ -} -FUNCTION {format.names.ed} -{ - format.names -} -FUNCTION {format.key} -{ empty$ - { key field.or.null } - { "" } - if$ -} - -FUNCTION {format.authors} -{ author "author" format.names -} -FUNCTION {get.bbl.editor} -{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ } - -FUNCTION {format.editors} -{ editor "editor" format.names duplicate$ empty$ 'skip$ - { - " " * - get.bbl.editor - "(" swap$ * ")" * - * - } - if$ -} -FUNCTION {format.doi} -{ doi "doi" bibinfo.check - duplicate$ empty$ 'skip$ - { - new.block - "\doi{" swap$ * "}" * - } - if$ -} -FUNCTION {format.note} -{ - note empty$ - { "" } - { note #1 #1 substring$ - duplicate$ "{" = - 'skip$ - { output.state mid.sentence = - { "l" } - { "u" } - if$ - change.case$ - } - if$ - note #2 global.max$ substring$ * "note" bibinfo.check - } - if$ -} - -FUNCTION {format.title} -{ title - duplicate$ empty$ 'skip$ - { "t" change.case$ } - if$ - "title" bibinfo.check -} -FUNCTION {format.full.names} -{'s := - "" 't := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr -% -% MANUAL: Removed comma before junior part. -% -% "{vv~}{ll}{, jj}" format.name$ - "{vv~}{ll}{ jj}" format.name$ - 't := - nameptr #1 > - { - namesleft #1 > - { ", " * t * } - { - s nameptr "{ll}" format.name$ duplicate$ "others" = - { 't := } - { pop$ } - if$ - t "others" = - { - " " * bbl.etal * - } - { - numnames #2 > - { "," * } - 'skip$ - if$ - bbl.and - space.word * t * - } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {author.editor.key.full} -{ author empty$ - { editor empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { editor format.full.names } - if$ - } - { author format.full.names } - if$ -} - -FUNCTION {author.key.full} -{ author empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { author format.full.names } - if$ -} - -FUNCTION {editor.key.full} -{ editor empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { editor format.full.names } - if$ -} - -FUNCTION {make.full.names} -{ type$ "book" = - type$ "inbook" = - or - 'author.editor.key.full - { type$ "proceedings" = - 'editor.key.full - 'author.key.full - if$ - } - if$ -} - -FUNCTION {output.bibitem} -{ newline$ - "\bibitem[{" write$ - label write$ - ")" make.full.names duplicate$ short.list = - { pop$ } - { * } - if$ - "}]{" * write$ - cite$ write$ - "}" write$ - newline$ - "" - before.all 'output.state := -} - -FUNCTION {if.digit} -{ duplicate$ "0" = - swap$ duplicate$ "1" = - swap$ duplicate$ "2" = - swap$ duplicate$ "3" = - swap$ duplicate$ "4" = - swap$ duplicate$ "5" = - swap$ duplicate$ "6" = - swap$ duplicate$ "7" = - swap$ duplicate$ "8" = - swap$ "9" = or or or or or or or or or -} -FUNCTION {n.separate} -{ 't := - "" - #0 'numnames := - { t empty$ not } - { t #-1 #1 substring$ if.digit - { numnames #1 + 'numnames := } - { #0 'numnames := } - if$ - t #-1 #1 substring$ swap$ * - t #-2 global.max$ substring$ 't := - numnames #5 = - { duplicate$ #1 #2 substring$ swap$ - #3 global.max$ substring$ - "," swap$ * * - } - 'skip$ - if$ - } - while$ -} -FUNCTION {n.dashify} -{ - n.separate - 't := - "" - { t empty$ not } - { t #1 #1 substring$ "-" = - { t #1 #2 substring$ "--" = not - { "--" * - t #2 global.max$ substring$ 't := - } - { { t #1 #1 substring$ "-" = } - { "-" * - t #2 global.max$ substring$ 't := - } - while$ - } - if$ - } - { t #1 #1 substring$ * - t #2 global.max$ substring$ 't := - } - if$ - } - while$ -} - -FUNCTION {word.in} -{ bbl.in capitalize - ":" * - " " * } - -FUNCTION {format.date} -{ year "year" bibinfo.check duplicate$ empty$ - { - "empty year in " cite$ * "; set to ????" * warning$ - pop$ "????" - } - 'skip$ - if$ - extra.label * - before.all 'output.state := - " (" swap$ * ")" * -} -FUNCTION {format.btitle} -{ title "title" bibinfo.check - duplicate$ empty$ 'skip$ - { - } - if$ -} -FUNCTION {either.or.check} -{ empty$ - 'pop$ - { "can't use both " swap$ * " fields in " * cite$ * warning$ } - if$ -} -FUNCTION {format.bvolume} -{ volume empty$ - { "" } - { bbl.volume volume tie.or.space.prefix - "volume" bibinfo.check * * - series "series" bibinfo.check - duplicate$ empty$ 'pop$ - { emphasize ", " * swap$ * } - if$ - "volume and number" number either.or.check - } - if$ -} -FUNCTION {format.number.series} -{ volume empty$ - { number empty$ - { series field.or.null } - { series empty$ - { number "number" bibinfo.check } - { output.state mid.sentence = - { bbl.number } - { bbl.number capitalize } - if$ - number tie.or.space.prefix "number" bibinfo.check * * - bbl.in space.word * - series "series" bibinfo.check * - } - if$ - } - if$ - } - { "" } - if$ -} - -FUNCTION {format.edition} -{ edition duplicate$ empty$ 'skip$ - { - output.state mid.sentence = - { "l" } - { "t" } - if$ change.case$ - "edition" bibinfo.check - " " * bbl.edition * - } - if$ -} -INTEGERS { multiresult } -FUNCTION {multi.page.check} -{ 't := - #0 'multiresult := - { multiresult not - t empty$ not - and - } - { t #1 #1 substring$ - duplicate$ "-" = - swap$ duplicate$ "," = - swap$ "+" = - or or - { #1 'multiresult := } - { t #2 global.max$ substring$ 't := } - if$ - } - while$ - multiresult -} -FUNCTION {format.pages} -{ pages duplicate$ empty$ 'skip$ - { duplicate$ multi.page.check - { - bbl.pages swap$ - n.dashify - } - { - bbl.page swap$ - } - if$ - tie.or.space.prefix - "pages" bibinfo.check - * * - } - if$ -} -FUNCTION {format.journal.pages} -{ pages duplicate$ empty$ 'pop$ - { swap$ duplicate$ empty$ - { pop$ pop$ format.pages } - { - ", " * - swap$ - n.dashify - "pages" bibinfo.check - * - } - if$ - } - if$ -} -FUNCTION {format.journal.eid} -{ eid "eid" bibinfo.check - duplicate$ empty$ 'pop$ - { swap$ duplicate$ empty$ 'skip$ - { - ", " * - } - if$ - swap$ * - } - if$ -} -FUNCTION {format.vol.num.pages} -{ volume field.or.null - duplicate$ empty$ 'skip$ - { - "volume" bibinfo.check - } - if$ - bolden - number "number" bibinfo.check duplicate$ empty$ 'skip$ - { - swap$ duplicate$ empty$ - { "there's a number but no volume in " cite$ * warning$ } - 'skip$ - if$ - swap$ - "(" swap$ * ")" * - } - if$ * - eid empty$ - { format.journal.pages } - { format.journal.eid } - if$ -} - -FUNCTION {format.chapter.pages} -{ chapter empty$ - 'format.pages - { type empty$ - { bbl.chapter } - { type "l" change.case$ - "type" bibinfo.check - } - if$ - chapter tie.or.space.prefix - "chapter" bibinfo.check - * * - pages empty$ - 'skip$ - { ", " * format.pages * } - if$ - } - if$ -} - -FUNCTION {format.booktitle} -{ - booktitle "booktitle" bibinfo.check -} -FUNCTION {format.in.ed.booktitle} -{ format.booktitle duplicate$ empty$ 'skip$ - { - format.bvolume duplicate$ empty$ 'pop$ - { ", " swap$ * * } - if$ - editor "editor" format.names.ed duplicate$ empty$ 'pop$ - { - " " * - get.bbl.editor - "(" swap$ * ") " * - * swap$ - * } - if$ - word.in swap$ * - } - if$ -} -FUNCTION {format.thesis.type} -{ type duplicate$ empty$ - 'pop$ - { swap$ pop$ - "t" change.case$ "type" bibinfo.check - } - if$ -} -FUNCTION {format.tr.number} -{ number "number" bibinfo.check - type duplicate$ empty$ - { pop$ bbl.techrep } - 'skip$ - if$ - "type" bibinfo.check - swap$ duplicate$ empty$ - { pop$ "t" change.case$ } - { tie.or.space.prefix * * } - if$ -} -FUNCTION {format.article.crossref} -{ - word.in - " \cite{" * crossref * "}" * -} -FUNCTION {format.book.crossref} -{ volume duplicate$ empty$ - { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ - pop$ word.in - } - { bbl.volume - capitalize - swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word * - } - if$ - " \cite{" * crossref * "}" * -} -FUNCTION {format.incoll.inproc.crossref} -{ - word.in - " \cite{" * crossref * "}" * -} -FUNCTION {format.org.or.pub} -{ 't := - "" - address empty$ t empty$ and - 'skip$ - { - t empty$ - { address "address" bibinfo.check * - } - { t * - address empty$ - 'skip$ - { ", " * address "address" bibinfo.check * } - if$ - } - if$ - } - if$ -} -FUNCTION {format.publisher.address} -{ publisher "publisher" bibinfo.warn format.org.or.pub -} - -FUNCTION {format.organization.address} -{ organization "organization" bibinfo.check format.org.or.pub -} - -FUNCTION {article} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { - journal - "journal" bibinfo.check - "journal" output.check - add.blank - format.vol.num.pages output - format.date "year" output.check - } - { format.article.crossref output.nonnull - format.pages output - } - if$ - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} -FUNCTION {book} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check - editor format.key output - add.colon - } - { format.authors output.nonnull - add.colon - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - new.block - format.btitle "title" output.check - crossref missing$ - { format.bvolume output - new.block - format.number.series output - format.edition output - new.sentence - format.publisher.address output - } - { - new.block - format.book.crossref output.nonnull - } - if$ - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} -FUNCTION {booklet} -{ output.bibitem - format.authors output - author format.key output - add.colon - new.block - format.title "title" output.check - new.block - howpublished "howpublished" bibinfo.check output - address "address" bibinfo.check output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {inbook} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check - editor format.key output - add.colon - } - { format.authors output.nonnull - add.colon - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - new.block - format.btitle "title" output.check - crossref missing$ - { - format.bvolume output - format.chapter.pages "chapter and pages" output.check - new.block - format.number.series output - format.edition output - new.sentence - format.publisher.address output - } - { - format.chapter.pages "chapter and pages" output.check - new.block - format.book.crossref output.nonnull - } - if$ - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {incollection} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - format.number.series output - format.edition output - format.chapter.pages output - new.sentence - format.publisher.address output - format.date "year" output.check - } - { format.incoll.inproc.crossref output.nonnull - format.chapter.pages output - } - if$ - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} -FUNCTION {inproceedings} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - format.number.series output - format.pages output - new.sentence - publisher empty$ - { format.organization.address output } - { organization "organization" bibinfo.check output - format.publisher.address output - } - if$ - format.date "year" output.check - } - { format.incoll.inproc.crossref output.nonnull - format.pages output - } - if$ - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} -FUNCTION {conference} { inproceedings } -FUNCTION {manual} -{ output.bibitem - format.authors output - author format.key output - add.colon - new.block - format.btitle "title" output.check - organization address new.block.checkb - organization "organization" bibinfo.check output - address "address" bibinfo.check output - format.edition output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {mastersthesis} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title - "title" output.check - new.block - bbl.mthesis format.thesis.type output.nonnull - school "school" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {misc} -{ output.bibitem - format.authors output - author format.key output - add.colon - new.block - format.title output - new.block - howpublished "howpublished" bibinfo.check output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} -FUNCTION {phdthesis} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title - "title" output.check - new.block - bbl.phdthesis format.thesis.type output.nonnull - school "school" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {proceedings} -{ output.bibitem - format.editors output - editor format.key output - add.colon - new.block - format.btitle "title" output.check - format.bvolume output - format.number.series output - new.sentence - publisher empty$ - { format.organization.address output } - { organization "organization" bibinfo.check output - format.publisher.address output - } - if$ - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {techreport} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title - "title" output.check - new.block - format.tr.number output.nonnull - institution "institution" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note output - fin.entry -} - -FUNCTION {unpublished} -{ output.bibitem - format.authors "author" output.check - author format.key output - add.colon - new.block - format.title "title" output.check - format.date "year" output.check - format.doi output - new.block - format.url output - new.block - format.note "note" output.check - fin.entry -} - -FUNCTION {default.type} { misc } -READ -FUNCTION {sortify} -{ purify$ - "l" change.case$ -} -INTEGERS { len } -FUNCTION {chop.word} -{ 's := - 'len := - s #1 len substring$ = - { s len #1 + global.max$ substring$ } - 's - if$ -} -FUNCTION {format.lab.names} -{ 's := - "" 't := -% -% MANUAL: Removed comma before junior part. -% -% s #1 "{vv~}{ll}{, jj}" format.name$ - s #1 "{vv~}{ll}{ jj}" format.name$ - s num.names$ duplicate$ - #2 > - { pop$ - " " * bbl.etal * - } - { #2 < - 'skip$ - { s #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = - { - " " * bbl.etal * - } - { bbl.and space.word * s #2 "{vv~}{ll}" format.name$ - * } - if$ - } - if$ - } - if$ -} - -FUNCTION {author.key.label} -{ author empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { author format.lab.names } - if$ -} - -FUNCTION {author.editor.key.label} -{ author empty$ - { editor empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { editor format.lab.names } - if$ - } - { author format.lab.names } - if$ -} - -FUNCTION {editor.key.label} -{ editor empty$ - { key empty$ - { cite$ #1 #3 substring$ } - 'key - if$ - } - { editor format.lab.names } - if$ -} - -FUNCTION {calc.short.authors} -{ type$ "book" = - type$ "inbook" = - or - 'author.editor.key.label - { type$ "proceedings" = - 'editor.key.label - 'author.key.label - if$ - } - if$ - 'short.list := -} - -FUNCTION {calc.label} -{ calc.short.authors - short.list - "(" - * - year duplicate$ empty$ - { pop$ "????" } - { purify$ #-1 #4 substring$ } - if$ - * - 'label := -} - -FUNCTION {sort.format.names} -{ 's := - #1 'nameptr := - "" - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr - "{ll{ }}{ f{ }}{ jj{ }}" - format.name$ 't := - nameptr #1 > - { - " " * - namesleft #1 = t "others" = and - { "zzzzz" * } - { t sortify * } - if$ - } - { t sortify * } - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {sort.format.title} -{ 't := - "A " #2 - "An " #3 - "The " #4 t chop.word - chop.word - chop.word - sortify - #1 global.max$ substring$ -} -FUNCTION {author.sort} -{ author empty$ - { key empty$ - { "to sort, need author or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { author sort.format.names } - if$ -} -FUNCTION {author.editor.sort} -{ author empty$ - { editor empty$ - { key empty$ - { "to sort, need author, editor, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { editor sort.format.names } - if$ - } - { author sort.format.names } - if$ -} -FUNCTION {editor.sort} -{ editor empty$ - { key empty$ - { "to sort, need editor or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { editor sort.format.names } - if$ -} -FUNCTION {presort} -{ calc.label - label sortify - " " - * - type$ "book" = - type$ "inbook" = - or - 'author.editor.sort - { type$ "proceedings" = - 'editor.sort - 'author.sort - if$ - } - if$ - #1 entry.max$ substring$ - 'sort.label := - sort.label - * - " " - * - title field.or.null - sort.format.title - * - #1 entry.max$ substring$ - 'sort.key$ := -} - -ITERATE {presort} -SORT -STRINGS { last.label next.extra } -INTEGERS { last.extra.num number.label } -FUNCTION {initialize.extra.label.stuff} -{ #0 int.to.chr$ 'last.label := - "" 'next.extra := - #0 'last.extra.num := - #0 'number.label := -} -FUNCTION {forward.pass} -{ last.label label = - { last.extra.num #1 + 'last.extra.num := - last.extra.num int.to.chr$ 'extra.label := - } - { "a" chr.to.int$ 'last.extra.num := - "" 'extra.label := - label 'last.label := - } - if$ - number.label #1 + 'number.label := -} -FUNCTION {reverse.pass} -{ next.extra "b" = - { "a" 'extra.label := } - 'skip$ - if$ - extra.label 'next.extra := - extra.label - duplicate$ empty$ - 'skip$ - { "{\natexlab{" swap$ * "}}" * } - if$ - 'extra.label := - label extra.label * 'label := -} -EXECUTE {initialize.extra.label.stuff} -ITERATE {forward.pass} -REVERSE {reverse.pass} -FUNCTION {bib.sort.order} -{ sort.label - " " - * - year field.or.null sortify - * - " " - * - title field.or.null - sort.format.title - * - #1 entry.max$ substring$ - 'sort.key$ := -} -ITERATE {bib.sort.order} -SORT -FUNCTION {begin.bib} -{ preamble$ empty$ - 'skip$ - { preamble$ write$ newline$ } - if$ - "\begin{thebibliography}{" number.label int.to.str$ * "}" * - write$ newline$ - "\providecommand{\natexlab}[1]{#1}" - write$ newline$ -% -% MANUAL: Removed \texttt from \url. -% -% "\providecommand{\url}[1]{\texttt{#1}}" - "\providecommand{\url}[1]{#1}" - write$ newline$ - "\providecommand{\urlprefix}{URL }" - write$ newline$ - "\expandafter\ifx\csname urlstyle\endcsname\relax" - write$ newline$ -% -% MANUAL: Changed "doi:" to "DOI~". -% -% " \providecommand{\doi}[1]{doi:\discretionary{}{}{}#1}\else" - " \providecommand{\doi}[1]{DOI~\discretionary{}{}{}#1}\else" - write$ newline$ -% -% MANUAL: Changed "doi:" to "DOI~". -% -% " \providecommand{\doi}{doi:\discretionary{}{}{}\begingroup \urlstyle{rm}\Url}\fi" - " \providecommand{\doi}{DOI~\discretionary{}{}{}\begingroup \urlstyle{rm}\Url}\fi" - write$ newline$ -} -EXECUTE {begin.bib} -EXECUTE {init.state.consts} -ITERATE {call.type$} -FUNCTION {end.bib} -{ newline$ - "\end{thebibliography}" write$ newline$ -} -EXECUTE {end.bib} -%% End of customized bst file -%% -%% End of file `spmpscinat.bst'. diff --git a/examples/scholarly_paper/ROOTS b/examples/scholarly_paper/ROOTS old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy old mode 100755 new mode 100644 index 40adac7..9980b12 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -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 diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy old mode 100755 new mode 100644 index 56646ed..8d530b0 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -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 diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png old mode 100755 new mode 100644 index 528a8f0..c8a3461 Binary files a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png old mode 100755 new mode 100644 index 0773ac2..ead484e Binary files a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100755 new mode 100644 index 3fe072d..a99c97c Binary files a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png old mode 100755 new mode 100644 index 7e33ee9..2ca944d Binary files a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png differ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/MyCommentedIsabelle.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/MyCommentedIsabelle.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/definition-use-CSP-pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/definition-use-CSP-pdf.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg b/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib old mode 100755 new mode 100644 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.mst b/examples/technical_report/Isabelle_DOF-Manual/document/root.mst old mode 100755 new mode 100644 diff --git a/examples/technical_report/ROOTS b/examples/technical_report/ROOTS old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty old mode 100755 new mode 100644 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.bib b/examples/technical_report/TR_my_commented_isabelle/document/root.bib old mode 100755 new mode 100644 diff --git a/src/DOF/.Isa_DOF.thy.marks b/src/DOF/.Isa_DOF.thy.marks deleted file mode 100644 index 36df4bd..0000000 Binary files a/src/DOF/.Isa_DOF.thy.marks and /dev/null differ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy old mode 100755 new mode 100644 diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 9cb7611..d54a16e 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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 diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy old mode 100755 new mode 100644 diff --git a/src/ROOT b/src/ROOT old mode 100755 new mode 100644 index 1b5f2f3..802046e --- a/src/ROOT +++ b/src/ROOT @@ -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" diff --git a/src/ROOTS b/src/ROOTS old mode 100755 new mode 100644 diff --git a/src/Tools/mkroot_DOF b/src/Tools/mkroot_DOF index 533c547..d1dfe9d 100755 --- a/src/Tools/mkroot_DOF +++ b/src/Tools/mkroot_DOF @@ -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 diff --git a/src/document-templates/root-eptcs-UNSUPPORTED.tex b/src/document-templates/root-eptcs-UNSUPPORTED.tex old mode 100755 new mode 100644 diff --git a/src/document-templates/root-lipics-v2021.tex b/src/document-templates/root-lipics-v2021.tex old mode 100755 new mode 100644 diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex old mode 100755 new mode 100644 index 840364a..83258d5 --- a/src/document-templates/root-lncs.tex +++ b/src/document-templates/root-lncs.tex @@ -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} }}{} diff --git a/src/document-templates/root-scrartcl.tex b/src/document-templates/root-scrartcl.tex old mode 100755 new mode 100644 diff --git a/src/document-templates/root-scrreprt-modern.tex b/src/document-templates/root-scrreprt-modern.tex old mode 100755 new mode 100644 diff --git a/src/document-templates/root-scrreprt.tex b/src/document-templates/root-scrreprt.tex old mode 100755 new mode 100644 diff --git a/src/document-templates/root-svjour3-UNSUPPORTED.tex b/src/document-templates/root-svjour3-UNSUPPORTED.tex old mode 100755 new mode 100644 diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy old mode 100755 new mode 100644 diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty old mode 100755 new mode 100644 diff --git a/src/ontologies/math_exam/DOF-math_exam.sty b/src/ontologies/math_exam/DOF-math_exam.sty deleted file mode 100755 index 561c733..0000000 --- a/src/ontologies/math_exam/DOF-math_exam.sty +++ /dev/null @@ -1,102 +0,0 @@ -%% Copyright (C) 2018 The University of Sheffield -%% 2018 The University of Paris-Saclay -%% -%% 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{DOF-math_exam} - [<isadofltxversion>% - Document-Type Support Framework for math classes.] - -\RequirePackage{DOF-COL} -\usepackage{sfmath} -\usepackage{amsmath} -\usepackage{lastpage} -\usepackage{scrlayer-scrpage} -\usepackage{exercise} - -\cfoot{\small\textnormal{Page \thepage\ of \pageref{LastPage}}} - -\def\dof@author{}% -\def\dof@affiliation{}% - -\AtBeginDocument{% - \author{\dof@author} -% \institute{\dof@affiliation} -} - - -\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}} -\def\leftaddaux#1#2#3{\gdef#3{#1#2}} - -\newcommand{\addauthor}[1]{% - \ifthenelse{\equal{\dof@author}{}}{% - \gdef\dof@author{#1}% - }{% - \leftadd\dof@author{\protect\and #1}% - } -} - -\newkeycommand\isaDofSectionAuthor[label=,type=,affiliation=,email=][1]{% - \immediate\write\@auxout{\noexpand\addauthor{#1}}% -} - -\newkeycommand\isaDofTextHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{% - \immediate\write\@auxout{\noexpand\title{#1}}% -} - -\newkeycommand\isaDofSectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{% - \immediate\write\@auxout{\noexpand\title{#1}}% -} - -\newkeycommand\isaDofSubsectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{% - \immediate\write\@auxout{\noexpand\title{#1}}% -} - -\newkeycommand\isaDofTextAnswerFormalStep[label=,type=,justification=,term=][1]{% - #1 -} - -\newkeycommand\isaDofTextAnswerYesNo[label=,type=,step_label=,yes_no=][1]{% - #1 -} - -\newkeycommand\isaDofTextExamitem[label=,type=,concerns=][1]{% - #1 -} - -\newkeycommand\isaDofTextTask[label=,type=,level=,type=,subitems=concerns=,mark=][1]{% - #1 -} - -\newkeycommand\isaDofSubsubsectionExercise[label=,type=,Exercise.content=,concerns=,][1]{% - \begin{Exercise} - #1 - \end{Exercise} -} - -\newkeycommand\isaDofSubsubsectionValidation[label=,type=,tests=,proofs=][1]{% - #1 -} - -\newkeycommand\isaDofSubsubsectionSolution[label=,type=,content=,valids=,concerns=][1]{% - \begin{Answer} - #1 - \end{Answer} -} - -\newkeycommand\isaDofSubsubsectionMathExam[label=,type=,content=,global_grade=][1]{% - #1 -} - - -\newkeycommand\isaDofOpenMonitorMathExam[label=,type=]{} -\newkeycommand\isaDofCloseMonitorMathExam[label=,type=]{} diff --git a/src/ontologies/math_exam/Nmath_exam.thy b/src/ontologies/math_exam/Nmath_exam.thy deleted file mode 100755 index 10d8d42..0000000 --- a/src/ontologies/math_exam/Nmath_exam.thy +++ /dev/null @@ -1,195 +0,0 @@ -(************************************************************************* - * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay - * 2018 The University of Sheffield - * - * License: - * This program can be redistributed and/or modified under the terms - * of the 2-clause BSD-style license. - * - * SPDX-License-Identifier: BSD-2-Clause - *************************************************************************) - -theory Nmath_exam - imports "../../DOF/Isa_COL" -begin - -text\<open>In our scenario, content has four different types of addressees: -\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam, -\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam, -\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for -\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for - feasibility and non-ambiguity. - -Note that the latter quality assurance mechanism is used in many universities, -where for organizational reasons the execution of an exam takes place in facilities -where the author of the exam is not expected to be physically present. -\<close> - - -datatype content_class = setter | checker | external_examiner | student - -text\<open>Tasks, Answers and Solutions are grouped into the \<^emph>\<open>categories\<close> -\<^enum> \<open>main\<close> and -\<^enum> \<open>sub\<close>. \<close> - -datatype category = main | sub - -doc_class author = - affiliation :: "string" - roles :: "content_class set" - email :: "string" - -doc_class context_description = - label :: string - -doc_class exam_item = - level :: "int option" - concerns :: "content_class set" - visible_for :: "content_class set" - -doc_class header = exam_item + - date :: string - authors :: "author list" - timeAllowed :: int (* minutes *) - - -datatype prog_lang = python | C | java | Haskell | SML - - -doc_class marking = exam_item + - marks :: int - -doc_class answer_element = exam_item + - cat :: category -(* justification :: string - "term" :: "string" *) - - -doc_class text_answer = answer_element + - "term" :: "string" - -doc_class program_text = answer_element + - prog_lang :: prog_lang - pre_filled :: "string" <= "\<open>This is a text with \<alpha>, \<beta>, \<gamma>\<close>" - -doc_class formula_text = answer_element + - "term" :: "string" - -doc_class checkbox = exam_item + - "value" :: "bool option" - -doc_class checkboxes = answer_element + - marks :: int - accepts "\<lbrace>checkbox\<rbrace>\<^sup>+" - -doc_class radiobutton = exam_item + - "value" :: "bool option" - "term" :: "string" - -doc_class radiobuttons = answer_element + - "term" :: "string" - accepts "\<lbrace>radiobutton\<rbrace>\<^sup>+ " - -datatype opn = eq | equiv | refines | refined_by - -doc_class equational_derivation = answer_element + - eq_deriv :: "(opn option \<times> term option) list" - -(* these two could be refined substantially *) -doc_class proof_derivation = answer_element + - "term" :: "term list" - -doc_class answer = exam_item + - cat :: category - accepts "\<lbrace>answer_element\<rbrace>\<^sup>+ " - - -datatype task_type = formal | informal | mixed - -doc_class task = exam_item + - cat :: category - local_grade :: marking - type :: task_type - concerns :: "content_class set" <= "{setter,student,checker,external_examiner}" - mark :: int - -doc_class validation = - tests :: "term list" <="[]" - proofs :: "thm list" <="[]" - -doc_class solution = exam_item + - cat :: category - motivation :: string - valids :: "validation list" - objectives :: string - responds_to :: answer - concerns :: "content_class set" <= "{setter,checker,external_examiner}" - accepts "\<lbrace>answer_element\<rbrace>\<^sup>+" - - - -doc_class exercise = exam_item + - concerns :: "content_class set" <= "{setter,student,checker,external_examiner}" - accepts "header ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ context_description ~~ \<lbrace>task ~~ answer\<rbrace>\<^sup>+ ~~ \<lbrace>solution\<rbrace>\<^sup>+" (* PSud style*) -(* accepts "\<lbrace>task ~~ answer ~~ \<lbrace>solution\<rbrace>\<^sup>+ \<rbrace>\<^sup>+ " (*Exeter style *) *) - - - -ML\<open>fun check_exercise_inv_1 oid {is_monitor} ctxt = - let fun get_attr oid attr = AttributeAccess.compute_attr_access ctxt attr oid @{here} @{here} - (* val term = AttributeAccess.compute_attr_access ctxt "trace" oid @{here} @{here} *) - fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) - val string_pair_list = map conv (HOLogic.dest_list (get_attr oid "trace" )) - val cid_list = map fst string_pair_list - val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) - fun is_task x = DOF_core.is_subclass ctxt' x "Nmath_exam.task" - fun is_answer x = DOF_core.is_subclass ctxt' x "Nmath_exam.answer" - val task_answer_part = (filter (fn x => is_task x orelse is_answer x) cid_list) - val _ = case get_attr (hd task_answer_part) "cat" of - @{term "main"} => () - | _ => error("class exercise invariant violation: must start with main category. ") - fun check_match [] = () - |check_match (task_id::answer_id::S) = - (if get_attr task_id "cat" = get_attr answer_id "cat" - then check_match S - else error("class exercise invariant violation: \ - \ task and answer category does not match. ")) - val _ = check_match task_answer_part - in true end -\<close> - -setup\<open>DOF_core.update_class_invariant - "Nmath_exam.exercise" - check_exercise_inv_1\<close> - - -doc_class math_exam = - global_grade :: int - accepts "header ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ context_description ~~ \<lbrace>exercise\<rbrace>\<^sup>+ " - - - -text\<open> Invariants (not yet implemented): - -\<^enum> the task list must start with a \<open>main\<close> category. - -\<^enum> \<open>solutions\<close> must structurally match to answer blocks, i.e. coincide in - category and corresponding answer elements - -\<^enum> one-to-n relation between answer_elements and solutions - -\<^enum> invariants over markings and grades : sub-task must sum up to task grades, exo - marks to the global grade. - -\<^enum> distribution constraints: subtask should have no more than 25 % of overall grade. - -\<close> - - - - -(*>*) -end -(*<*) diff --git a/src/ontologies/math_exam/math_exam.thy b/src/ontologies/math_exam/math_exam.thy deleted file mode 100755 index 3c13235..0000000 --- a/src/ontologies/math_exam/math_exam.thy +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************* - * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay - * 2018 The University of Sheffield - * - * License: - * This program can be redistributed and/or modified under the terms - * of the 2-clause BSD-style license. - * - * SPDX-License-Identifier: BSD-2-Clause - *************************************************************************) - -theory math_exam - imports "../../DOF/Isa_COL" -begin - -(*<<*) -text\<open>In our scenario, content has four different types of addressees: -\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam, -\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam, -\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for -\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for - feasibility and non-ambiguity. - -Note that the latter quality assurance mechanism is used in many universities, -where for organizational reasons the execution of an exam takes place in facilities -where the author of the exam is not expected to be physically present. -\<close> - - -datatype ContentClass = - setter (* \<open>the 'author' of the exam\<close> *) - | checker (* \<open>the 'proof-reader' of the exam\<close> *) - | externalExaminer (* \<open>an external 'proof-reader' of the exam\<close> *) - | student (* \<open>the victim ;-) ... \<close> *) - - -doc_class Author = - affiliation :: "string" - email :: "string" - - - -datatype Subject = - algebra | geometry | statistical | analysis - -datatype Level = - oneStar | twoStars | threeStars - - -datatype Grade = - A1 | A2 | A3 - - -doc_class Exam_item = - level :: "int option" - concerns :: "ContentClass set" - -doc_class Header = Exam_item + - examSubject :: "(Subject) list" - date :: string - timeAllowed :: int (* minutes *) - - -type_synonym SubQuestion = string - -doc_class Answer_Formal_Step = Exam_item + - justification :: string - "term" :: "string" - -doc_class Answer_YesNo = Exam_item + - step_label :: string - yes_no :: bool (* \<open>for checkboxes\<close> *) - -datatype Question_Type = - formal | informal | mixed - -doc_class Task = Exam_item + - local_grade :: Level - type :: Question_Type - subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list" - concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}" - mark :: int - - -doc_class Exercise = Exam_item + - content :: "(Task) list" - concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}" - - -text\<open>In many institutions, it makes sense to have a rigorous process of validation -for exam subjects : is the initial question correct ? Is a proof in the sense of the -question possible ? We model the possibility that the @{term setter} validates a -question by a sample proof validated by Isabelle. In our scenario this sample proofs -are completely @{emph \<open>intern\<close>}, i.e. not exposed to the students but just additional -material for the internal review process of the exam.\<close> - -doc_class Validation = - tests :: "term list" <="[]" - proofs :: "thm list" <="[]" - -doc_class Solution = Exam_item + - content :: "Exercise list" - valids :: "Validation list" - concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}" - -doc_class MathExam = - content :: "(Header + Author + Exercise) list" - global_grade :: Grade - accepts "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ " - -(*>>*) -end diff --git a/src/ontologies/math_paper/math_paper.thy b/src/ontologies/math_paper/math_paper.thy deleted file mode 100755 index bd6abf0..0000000 --- a/src/ontologies/math_paper/math_paper.thy +++ /dev/null @@ -1,116 +0,0 @@ -(************************************************************************* - * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay - * 2018 The University of Sheffield - * - * License: - * This program can be redistributed and/or modified under the terms - * of the 2-clause BSD-style license. - * - * SPDX-License-Identifier: BSD-2-Clause - *************************************************************************) - -chapter \<open>A Math Paper Ontology (obsolete vs. scholarly_paper)\<close> - -text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem -statements, proofs, etc. Isabelle is a lot of things, but it is an interactive theorem -proving environment after all ! So this ontology provides: -\<^item> declarations for textual descriptions of definitions, lemmas, theorems, assertions, ... - and the usual means for typed referencing on them, -\<^item> monitors allowing for filtering content; this means (typed) brackets that can be - put around formal content that is more or less relevant for different types of users, - \fixme{find nicer formulation} -\<^item> LaTeX support. \<close> - - -theory math_paper - imports "../../DOF/Isa_DOF" - -begin - -section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close> - -text\<open> These document classes are intended to present a number of key-elements -in mathematical papers and generate LaTeX in the style of, for example: -\begin{verbatim} -\begin{definition}[Dilating function] -A dilating function for a run \(\rho'\) is a function \(\mathbb{N} \longrightarrow \mathbb{N}\) -that satisfies: -\begin{enumerate} - \item \(f\) is strictly monotonic, so that the order of the instants in not changed in \(\rho'\); - \item \(\forall n.~f(n) \geq n\), so that instants are inserted into \(\rho\); - \item \(f(0) = 0\), so that no instant is inserted before the first one; - \item \(\forall n.~(\not\exists n_0.~f(n_0) = n) \Longrightarrow - (\forall c.~\neg\mathsf{ticks}(\rho'_{n}(c))\), - there is no tick in stuttering instants; - \item \(\forall n.~(\not\exists n_0.~f(n_0) = n+1) \Longrightarrow - (\forall c.~\mathsf{time}(\rho'_{n+1}(c)) = \mathsf{time}(\rho'_{n}(c)))\), - time does not elapse during stuttering instants; -\end{enumerate} -\end{definition} -\end{verbatim} -which are intended to \<^emph>\<open>complement\<close> Isabelle's formal content elements such as definitions, -lemmas and formal proofs. - -We are aware that there is a certain tension between the interest to have more formal checking in -a definition as the above one and the interest in a notationally more liberal presentation that hides -technical details imposed by strict formality (even at the price that a chosen notation may be -intuitive, but an abstraction that is, fi donc, technically incorrect). - -We argue that it should be up to the user to decide in each individual case how to draw this line ... \<close> - -doc_class formal_stmt = - property :: "term list" - -datatype relevance = key | vital | working | auxilliary | alternative - -doc_class "definition" = formal_stmt + - relevance :: "relevance option" - property :: "term list" <= "[]" - -text\<open>Which gives rise to a presentation like:\<close> -(*<*) -type_notation nat ("\<nat>") -(*>*) -text*[dil_fun :: "definition"]\<open>A dilating function for a run @{term "\<rho>"} is a function -@{typ "\<nat> \<Rightarrow> \<nat>"} that satisfies: -\<^enum> @{term "f"} is strictly monotonic ... -\<^enum> ... -\<^enum> ... -\<close> - - -doc_class assertion = formal_stmt + - relevance :: "relevance option" - properties :: "term list" <= "[]" - -doc_class "lemma" = formal_stmt + - relevance :: "relevance" - properties :: "term list" <= "[]" - -doc_class "theorem" = formal_stmt + - relevance :: "relevance" - properties :: "term list" <= "[]" - - -doc_class "corrollary" = formal_stmt + - relevance :: "relevance" - properties :: "term list" <= "[]" - -text\<open>This monitor is used to group formal content in a way to classify the -relevance. On the presentation level, this gives the possibility to adapt or omit -Isabelle/Isar lemma and theorem commands according to their relevance level. -By using inheritance, the document class @{text \<open>formal_content\<close>} can also be used -to introduce organisational information (for example: developer or tester or validator ) -as a systematic means to produce documents oriented to specific needs of user (sub-)groups.\<close> - -doc_class formal_content = - relevance :: "relevance" - accepts "\<lbrace>definition || assertion || lemma || theorem || corrollary \<rbrace>\<^sup>+" - - - - - -end diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy old mode 100755 new mode 100644 index c0ae4ba..9f86dd0 --- a/src/ontologies/ontologies.thy +++ b/src/ontologies/ontologies.thy @@ -16,8 +16,6 @@ theory imports "CENELEC_50128/CENELEC_50128" "Conceptual/Conceptual" - "math_exam/math_exam" - "math_paper/math_paper" "scholarly_paper/scholarly_paper" "small_math/small_math" "technical_report/technical_report" diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty old mode 100755 new mode 100644 diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty old mode 100755 new mode 100644 index f49feb3..a76812e --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -127,7 +127,7 @@ } } -\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text.scholarly_paper.author},#1]{\BODY}} +\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}} \provideisadof{text.scholarly_paper.author}% [label=,type=% ,scholarly_paper.author.email=% diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy old mode 100755 new mode 100644 index 90692b2..fc0410c --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -305,7 +305,7 @@ val _ = {markdown = true, body = true} (fn meta_args => fn thy => let - val ddc = Config.get_global thy Definition_default_class + val ddc = Config.get_global thy Lemma_default_class val use_Lemma_default = SOME(((ddc = "") ? (K "math_content")) ddc) in Onto_Macros.enriched_formal_statement_command @@ -317,7 +317,7 @@ val _ = {markdown = true, body = true} (fn meta_args => fn thy => let - val ddc = Config.get_global thy Definition_default_class + val ddc = Config.get_global thy Theorem_default_class val use_Theorem_default = SOME(((ddc = "") ? (K "math_content")) ddc) in Onto_Macros.enriched_formal_statement_command diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy old mode 100755 new mode 100644 diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty old mode 100755 new mode 100644 diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy old mode 100755 new mode 100644 diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy old mode 100755 new mode 100644 index b9d216d..5f33288 --- a/src/tests/AssnsLemmaThmEtc.thy +++ b/src/tests/AssnsLemmaThmEtc.thy @@ -15,8 +15,7 @@ theory AssnsLemmaThmEtc imports "Isabelle_DOF.Conceptual" - "Isabelle_DOF.math_paper" - "Isabelle_DOF.scholarly_paper" (* for assert notation *) + "Isabelle_DOF.scholarly_paper" begin section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close> diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy old mode 100755 new mode 100644 diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy old mode 100755 new mode 100644 diff --git a/src/tests/Concept_Example_Low_Level_Invariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy old mode 100755 new mode 100644 diff --git a/src/tests/Evaluation.thy b/src/tests/Evaluation.thy index 5313a90..2c7a4c0 100644 --- a/src/tests/Evaluation.thy +++ b/src/tests/Evaluation.thy @@ -200,9 +200,10 @@ text\<open>Assertions must be true, hence the error:\<close> assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*) term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close> -assert*[ass::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close> +assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close> -text\<open>@{A [display] "ass"}}\<close> +text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close> +text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close> assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close> diff --git a/src/tests/ROOT b/src/tests/ROOT old mode 100755 new mode 100644 diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy old mode 100755 new mode 100644 diff --git a/src/tests/figures/A.png b/src/tests/figures/A.png old mode 100755 new mode 100644 diff --git a/src/tests/figures/AnB.odp b/src/tests/figures/AnB.odp old mode 100755 new mode 100644 diff --git a/src/tests/figures/B.png b/src/tests/figures/B.png old mode 100755 new mode 100644