added notes by referees to comment about our changes
%\documentclass{svjour3}\documentclass{llncs}\usepackage{times}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}\usepackage{pdfsetup}\usepackage{tikz}\usepackage{pgf}\usepackage{verbdef}\usepackage{longtable}\usepackage{mathpartir}\urlstyle{rm}\isabellestyle{it}\renewcommand{\isastyle}{\isastyleminor}\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}\verbdef\singlearr|--->|\verbdef\doublearr|===>|\verbdef\tripple|###|\renewcommand{\isasymequiv}{$\dn$}\renewcommand{\isasymemptyset}{$\varnothing$}\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}\renewcommand{\isasymUnion}{$\bigcup$}\newcommand{\isasymsinglearr}{\singlearr}\newcommand{\isasymdoublearr}{\doublearr}\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{$^*$ Technical University of Munich, Germany}\maketitle\begin{abstract}Higher-Order Logic (HOL) is based on a small logic kernel, whose onlymechanism for extension is the introduction of safe definitions and ofnon-empty types. Both extensions are often performed in quotientconstructions. To ease the work involved with such quotient constructions, were-implemented in Isabelle/HOL the quotient package by Homeier. In doing so weextended his work in order to deal with compositions of quotients. Like hispackage, we designed our quotient package so that every step in a quotient constructioncan be performed separately and as a result we are able to specify completelythe procedure of lifting theorems from the raw level to the quotient level.The importance for programming language research is that many properties ofprogramming language calculi are easier to verify over $\alpha$-equated, or$\alpha$-quotient, terms, than over raw terms.\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: