iUpdated nach diskussion mit Achim

examples/math_exam/MathExam/ROOT

@@ -1,9 +1,12 @@
 session "MathExam" = "HOL" +
   options [document = pdf, document_output = "output"]
   theories [document = false]
-    "../../../ontologies/mathex_onto" 
+    (* Foo *)
+    "../../../ontologies/mathex_onto"
   theories
-     MathExam
+    MathExam
   document_files
+    "preamble.tex"
+    "llncs.cls"
     "root.tex"
     "build"

examples/math_exam/MathExam/document/root.tex

@@ -1,56 +1,106 @@
-\documentclass[11pt,a4paper]{article}
+%% Copyright (C) 2018 The University of Sheffield
-\usepackage{isabelle,isabellesym}
+%%               2018 The University of Paris-Sud
+%%
+%% 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 of the License, or any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%  
+%%   SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
 
-% further packages required for unusual symbols (see also
+%% Warning: Do Not Edit!
-% isabellesym.sty), use only when needed
+%% =====================
+%% This is the root file for the Isabelle/DOF configuration "scholarly_paper/lncs". 
+%% All customization and/or additional packages should be added to the file 
+%% preamble.tex. 
 
-%\usepackage{amssymb}
+\RequirePackage{ifvtex}
-  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+\documentclass{llncs}
-  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+\usepackage[T1]{fontenc}
-  %\<triangleq>, \<yen>, \<lozenge>
+\usepackage[utf8]{inputenc}
-
+\usepackage[USenglish]{babel}
-%\usepackage{eurosym}
+\usepackage{isabelle}
-  %for \<euro>
+\usepackage{xcolor}
-
+\usepackage{isabellesym}
-%\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{amsmath}
-  %for \<Sqinter>
+\usepackage{amssymb}
-
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
-%\usepackage{eufrak}
+\usepackage{DOF-scholarly_paper-lncs}
-  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
-
+\usepackage{xspace}
-%\usepackage{textcomp}
+\newcommand{\isadof}{Isabelle/DOF\xspace}
-  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+\usepackage{graphicx}
-  %\<currency>
+\usepackage{hyperref}
-
+\setcounter{tocdepth}{3} 
-% this should be the last package used
+\hypersetup{%
-\usepackage{pdfsetup}
+   bookmarksdepth=3
-
+  ,pdfpagelabels
-% urls in roman style, theory text in math-similar italics
+  ,pageanchor=false
+  ,bookmarksnumbered
+  ,plainpages=false
+} % more detailed digital TOC (aka bookmarks)
+\sloppy
+\allowdisplaybreaks[4]
 \urlstyle{rm}
 \isabellestyle{it}
+\usepackage[caption]{subfig}
+\usepackage[size=footnotesize]{caption}
 
-% for uniform font size
+\newcommand{\ie}{i.e.}
-%\renewcommand{\isastyle}{\isastyleminor}
+\newcommand{\eg}{e.g.}
 
+\renewcommand{\topfraction}{0.9}      % max fraction of floats at top
+\renewcommand{\bottomfraction}{0.8}   % max fraction of floats at bottom
+\setcounter{topnumber}{2}
+\setcounter{bottomnumber}{2}
+\setcounter{totalnumber}{4}     % 2 may work better
+\setcounter{dbltopnumber}{2}    % for 2-column pages
+\renewcommand{\dbltopfraction}{0.9}   % fit big float above 2-col. text
+\renewcommand{\textfraction}{0.07}    % allow minimal text w. figs
+\renewcommand{\floatpagefraction}{0.7}        % require fuller float pages
+\renewcommand{\dblfloatpagefraction}{0.7}     % require fuller float pages
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% Overrides the (rightfully issued) warning by Koma Script that \rm
+%%% etc. should not be used (they are deprecated since more than a
+%%% decade)
+  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
+  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
+  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
+  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
+  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{document}
+\selectlanguage{USenglish}%
+\renewcommand{\bibname}{References}%
+\renewcommand{\figurename}{Fig.}
+\renewcommand{\abstractname}{Abstract.}
+\renewcommand{\subsubsectionautorefname}{Sect.}
+\renewcommand{\subsectionautorefname}{Sect.}
+\renewcommand{\sectionautorefname}{Sect.}
+\renewcommand{\figureautorefname}{Fig.}
+\newcommand{\subtableautorefname}{\tableautorefname}
+\newcommand{\subfigureautorefname}{\figureautorefname}
+\newcommand{\lstnumberautorefname}{Line}
+
+
 
-\title{MathExam}
-\author{By bu}
 \maketitle
-
+\makeatother
-\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-% generated text of all theories
 \input{session}
-
 % optional bibliography
-%\bibliographystyle{abbrv}
+\IfFileExists{root.bib}{%
-%\bibliography{root}
+{\small   \renewcommand{\doi}[1]{}
+  \newcommand{\urlprefix}{}
 
+  \bibliographystyle{spmpscinat}
+  
+  \bibliography{root}
+}}{}
 \end{document}
 
 %%% Local Variables: