--- a/Quotient-Paper/Paper.thy	Sun Jun 13 06:34:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 06:45:20 2010 +0200
@@ -229,7 +229,7 @@
 
   We will also address the criticism by Paulson \cite{Paulson06} cited at the
   beginning of this section about having to collect theorems that are lifted from the raw
-  level to the quotient level. Our quotient package id the first one that is modular so that it
+  level to the quotient level. Our quotient package is the first one that is modular so that it
   allows to lift single theorems separately. This has the advantage for the
   user to develop a formal theory interactively an a natural progression. A
   pleasing result of the modularity is also that we are able to clearly