# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276499782 -7200
# Node ID 2a98980f749948bc1094b67486d9860c9b345daf
# Parent  6c4b544823965f8ea7f39d66632f3470b3274439
qpaper

diff -r 6c4b54482396 -r 2a98980f7499 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 08:25:03 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 09:16:22 2010 +0200
@@ -886,7 +886,7 @@
   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)"}
+  \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"}
   \end{isabelle}
 
   \noindent
@@ -895,7 +895,7 @@
   definitions:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "\<approx>"}
+  \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}
   \end{isabelle}
 
   \noindent
@@ -913,7 +913,7 @@
   Lets first take a simple theorem about addition on the raw level:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "plus_zero_raw: plus_raw (0, 0) x \<approx> x"}
+  \isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
   \end{isabelle}
 
   \noindent
@@ -921,7 +921,7 @@
   proof obligation is left, so let us prove it first:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "[quot_respect]: (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
+  \isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"}
   \end{isabelle}
 
   \noindent