# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276589292 -7200
# Node ID 1fd6809f5a44a0f6c9d7984336957992c0db7925
# Parent  3bcd715abd39ebb23d0b0536c18a7a645a608933
Definition of Respects.

diff -r 3bcd715abd39 -r 1fd6809f5a44 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 09:22:38 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 10:08:12 2010 +0200
@@ -353,6 +353,10 @@
       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
   \end{proposition}
 
+  \begin{definition}[Respects]
+  An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+  \end{definition}
+
   \noindent
   We will heavily rely on this part of Homeier's work including an extension 
   to deal with compositions of equivalence relations defined as follows
@@ -370,6 +374,7 @@
   the HOL type system). However, we can prove useful instances for compatible
   containers. We will show such example in Section \ref{sec:resp}.
 
+
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}