# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276581270 -7200
# Node ID 2a95188263ec955321c4710840f74dc9f413f18b
# Parent  d2ca79475103c202358dff181137997c9ab0e1ca# Parent  5ced6472ac3c388cd0a676b594b9fff7e9147c69
merge

diff -r d2ca79475103 -r 2a95188263ec Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 07:52:42 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 07:54:30 2010 +0200
@@ -366,7 +366,7 @@
 
   \noindent
   Unfortunately, restrictions in HOL's type-system prevent us from stating
-  and proving a quotient type theorem, like \ref{funquot}, for compositions 
+  and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions 
   of relations. However, we can prove all instances where @{text R\<^isub>1} and 
   @{text "R\<^isub>2"} are built up by constituent equivalence relations.
 *}