# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276404320 -7200
# Node ID 43e3e8075f3f1b530ee791afb3cb3e5e96c95585
# Parent  a827d36fa467deccb5374f528775b28b2bbf095a
minor

diff -r a827d36fa467 -r 43e3e8075f3f Quotient-Paper/Paper.thy
--- 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