\documentclass{svjour3}+ −
\usepackage{times}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
\usepackage{pdfsetup}+ −
+ −
+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
\renewcommand{\isastyle}{\isastyleminor}+ −
+ −
\begin{document}+ −
+ −
\title{Quotients Revisited for Isabelle/HOL}+ −
\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}+ −
\institute{$^*$ Technical University of Munich, Germany}+ −
\maketitle+ −
+ −
\begin{abstract}+ −
Higher-order logic (HOL) is based on a safe logic kernel, which + −
can only be extended by introducing new definitions and new types. + −
+ −
\end{abstract}+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
\bibliographystyle{abbrv}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −