# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1328027196 0
# Node ID a9a4baa7779f2b79a3c7e303b6b202e0ecc3b04a
# Parent  f4112721a4b9e41cde245802c147db5bda3b3492
2 typos found by John Wickerson in QPaper

diff -r f4112721a4b9 -r a9a4baa7779f Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Tue Jan 24 17:43:07 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Tue Jan 31 16:26:36 2012 +0000
@@ -437,7 +437,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
@@ -1294,7 +1294,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}
diff -r f4112721a4b9 -r a9a4baa7779f Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jan 24 17:43:07 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Tue Jan 31 16:26:36 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}