\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:+
−