diff -r ad725de6e39b -r b8dda31890ff Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Sun Jun 13 17:40:32 2010 +0200 +++ b/Quotient-Paper/Paper.thy Sun Jun 13 17:41:07 2010 +0200 @@ -352,7 +352,7 @@ holds (for the proof see \cite{Homeier05}). The next step is to lift definitions over the raw type to definitions over the - quotient type. For this we providing the declaration + quotient type. For this we provide the declaration \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \isacommand{quotient\_definition}~~@{text "c :: \"}~\isacommand{is}~@{text "c' :: \"}