\documentclass{svjour3}+
−
\usepackage{times}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
\usepackage{pdfsetup}+
−
\usepackage{tikz}+
−
%\usepackage{pgf}+
−
\usepackage{stmaryrd}+
−
\usepackage{verbdef}+
−
%\usepackage{longtable}+
−
\usepackage{mathpartir}+
−
%\newtheorem{definition}{Definition}+
−
%\newtheorem{proposition}{Proposition}+
−
%\newtheorem{lemma}{Lemma}+
−
+
−
\urlstyle{rm}+
−
\isabellestyle{rm}+
−
\renewcommand{\isastyleminor}{\rm}%+
−
\renewcommand{\isastyle}{\normalsize\rm}%+
−
\renewcommand{\isastylescript}{\it}+
−
\def\dn{\,\triangleq\,}+
−
\verbdef\singlearr|---->|+
−
\verbdef\doublearr|===>|+
−
\verbdef\tripple|###|+
−
+
−
\renewcommand{\isasymequiv}{$\triangleq$}+
−
\renewcommand{\isasymemptyset}{$\varnothing$}+
−
%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+
−
\renewcommand{\isasymUnion}{$\bigcup$}+
−
+
−
\newcommand{\isasymsinglearr}{$\mapsto$}+
−
\newcommand{\isasymdoublearr}{$\Mapsto$}+
−
\newcommand{\isasymtripple}{\tripple}+
−
+
−
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}+
−
+
−
\begin{document}+
−
+
−
\title{Quotients Revisited for Isabelle/HOL}+
−
\author{Cezary Kaliszyk \and Christian Urban}+
−
\institute{C.~Kaliszyk \at University of Tsukuba, Japan+
−
     \and C.~Urban \at Technical University of Munich, Germany}+
−
\date{Received: date / Accepted: date}+
−
+
−
\maketitle+
−
+
−
\begin{abstract}+
−
Higher-Order Logic (HOL) is based on a small logic kernel, whose only+
−
mechanism for extension is the introduction of safe definitions and of+
−
non-empty types. Both extensions are often performed in quotient+
−
constructions. To ease the work involved with such quotient constructions, we+
−
re-implemented in the %popular+
−
Isabelle/HOL theorem prover the quotient+
−
package by Homeier. In doing so we extended his work in order to deal with+
−
compositions of quotients and also specified completely the procedure+
−
of lifting theorems from the raw level to the quotient level.+
−
The importance for theorem proving is that many formal+
−
verifications, in order to be feasible, require a convenient reasoning infrastructure+
−
for quotient constructions.+
−
\end{abstract}+
−
+
−
%\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}+
−
+
−
\bibliographystyle{abbrv}+
−
\input{session}+
−
+
−
+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−