--- a/Quotient-Paper/Paper.thy	Mon Jun 14 07:55:02 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 08:25:03 2010 +0200
@@ -875,13 +875,18 @@
 text {*
 
   In this section we will show, a complete interaction with the quotient package
-  for lifting a theorem about integers. A user of our quotient package first
-  needs to define a relation on the raw type, by which the quotienting will be
-  performed. We give the same integer relation as the one presented in the
-  introduction:
+  for defining the type of integers by quotienting pairs of natural numbers and
+  lifting theorems to integers. Our quotient package is fully compatible with
+  Isabelle type classes, but for clarity we will not use them in this example.
+  In a larger formalization of integers using the type class mechanism would
+  provide many algebraic properties ``for free''.
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(x \<Colon> nat, y) \<approx> (u, v) = (x + v = u + y)"}
+  A user of our quotient package first needs to define a relation on
+  the raw type, by which the quotienting will be performed. We give
+  the same integer relation as the one presented in the introduction:
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) \<approx> (p, q) = (m + q = n + p)"}
   \end{isabelle}
 
   \noindent
@@ -889,37 +894,53 @@
   relation is an equivalence relation which is solved automatically using the
   definitions:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "\<approx>"}
   \end{isabelle}
 
   \noindent
   The user can then specify the constants on the quotient type:
 
-  @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
-  @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
-  @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{tabular}{@ {}l}
+  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
+  \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\
+  \isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\
+  \end{tabular}
+  \end{isabelle}
 
+  \noindent
   Lets first take a simple theorem about addition on the raw level:
 
-  @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{lemma}~~@{text "plus_zero_raw: plus_raw (0, 0) x \<approx> x"}
+  \end{isabelle}
 
+  \noindent
   When the user tries to lift a theorem about integer addition, the respectfulness
   proof obligation is left, so let us prove it first:
-  
-  @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
 
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{lemma}~~@{text "[quot_respect]: (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
+  \end{isabelle}
+
+  \noindent
   Can be proved automatically by the system just by unfolding the definition
-  of @{term "op \<Longrightarrow>"}.
-
+  of @{text "op \<Longrightarrow>"}.
   Now the user can either prove a lifted lemma explicitly:
 
-  @{text "lemma 0 + i = i by lifting plus_zero_raw"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
+  \end{isabelle}
 
+  \noindent
   Or in this simple case use the automated translation mechanism:
 
-  @{text "thm plus_zero_raw[quot_lifted]"}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
+  \end{isabelle}
 
+  \noindent
   obtaining the same result.
 *}