# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276443667 -7200
# Node ID b8dda31890ff88f18e30630ebe128a0fd82fd697
# Parent  ad725de6e39be8ee6cbb51d743abbd6589298806
tuned

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