# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276317327 -7200
# Node ID cbffed7d81bdf53024ab1c8cbe11a2ca3a43cf8e
# Parent  f5b6f9d8a882efc966422b8438f307394b914737
Fix integer relation.

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