--- a/Quotient-Paper/Paper.thy	Thu Jun 02 15:35:33 2011 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Jun 02 16:15:18 2011 +0100
@@ -106,7 +106,7 @@
   theorem provers many questions concerning them are far from settled. In
   this paper we address the question of how to establish a convenient reasoning 
   infrastructure
-  for quotient constructions in the Isabelle/HOL, 
+  for quotient constructions in the Isabelle/HOL 
   theorem prover. Higher-Order Logic (HOL) consists
   of a small number of axioms and inference rules over a simply-typed
   term-language. Safe reasoning in HOL is ensured by two very restricted
@@ -531,7 +531,7 @@
   equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
   "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
   \eqref{listequiv}, respectively (the proofs about being equivalence
-  relations is omitted).  Given this data, we define for declarations shown in
+  relations are omitted).  Given this data, we define for declarations shown in
   \eqref{typedecl} the quotient types internally as
   
   \begin{isabelle}\ \ \ \ \ %%%