--- 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}
--- 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}