--- 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 :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}