# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276494902 -7200
# Node ID ff997de1bd73cae2ca5398e96b2f6f9a1a078f1e
# Parent  8ddf1330f2edf4595f7f5184f7873ccbc1f0d992
qpaper/examples

diff -r 8ddf1330f2ed -r ff997de1bd73 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 04:38:25 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 07:55:02 2010 +0200
@@ -874,17 +874,26 @@
 
 text {*
 
-  A user of our quotient package first needs to define an equivalence relation:
+  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:
 
-  @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}
-
-  Then the user defines a quotient type:
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(x \<Colon> nat, y) \<approx> (u, v) = (x + v = u + y)"}
+  \end{isabelle}
 
-  @{text "quotient_type int = (nat \<times> nat) / \<approx>"}
+  \noindent
+  Next the quotient type is defined. This leaves a proof obligation that the
+  relation is an equivalence relation which is solved automatically using the
+  definitions:
 
-  Which leaves a proof obligation that the relation is an equivalence relation,
-  that can be solved with the automatic tactic with two definitions.
+  \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)"}