diff -r 54eea17575e6 -r 69b4eb4b12c6 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 01 15:48:25 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 01 15:58:59 2010 +0200 @@ -36,7 +36,11 @@ section {* Introduction *} text {* - {\hfill quote by Larry}\bigskip + \begin{flushright} + {\em ``Not using a [quotient] package has its advantages: we do not have to\\ + collect all the theorems we shall ever want into one giant list;''}\\ + Paulson \cite{Paulson06} + \end{flushright}\smallskip \noindent Isabelle is a generic theorem prover in which many logics can be implemented.