--- a/Quotient-Paper/Paper.thy	Fri Feb 03 15:47:47 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Fri Feb 03 15:51:55 2012 +0000
@@ -428,7 +428,7 @@
 
   \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
   @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
-  and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+  and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}.
   \end{definition}
 
   The central definition in Homeier's work \cite{Homeier05} relates equivalence 
@@ -1284,7 +1284,7 @@
 
   \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\
   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
   \end{tabular}
   \end{isabelle}