diff -r f5b6f9d8a882 -r cbffed7d81bd Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jun 12 02:36:49 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 12 06:35:27 2010 +0200
@@ -63,7 +63,7 @@
   integers in Isabelle/HOL are constructed by a quotient construction over the
   type @{typ "nat \<times> nat"} and the equivalence relation
 
-  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
+  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}
 
   \noindent
   This constructions yields the new type @{typ int} and definitions for @{text