%% Copyright (c) 2019 University of Exeter
%%               2018-2019 University of Paris-Saclay
%%               2018-2019 The University of Sheffield
%%
%% 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

%%   <isadofltxversion>

%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lncs class.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.

\RequirePackage{ifvtex}
\documentclass{llncs}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[USenglish]{babel}
\usepackage{isabelle}
\usepackage{xcolor}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\IfFileExists{DOF-core.sty}{}{%
  \PackageError{DOF-core}{Isabelle/DOF not installed. 
    This is a Isabelle_DOF project. The document preparation requires
    the Isabelle_DOF component from:
    <isadofurl>
  }{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3} 
\hypersetup{%
   bookmarksdepth=3
  ,pdfpagelabels
  ,pageanchor=true
  ,bookmarksnumbered
  ,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}

\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

\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}



\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
{\small   \renewcommand{\doi}[1]{}
  \newcommand{\urlprefix}{}

  \bibliographystyle{splncs04}
  
  \bibliography{root}
}}{}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: