# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276577433 -7200
# Node ID 5ced6472ac3c388cd0a676b594b9fff7e9147c69
# Parent  ec7bc96a04b45263c0ca0a037f4b448075c3d08b
tuned

diff -r ec7bc96a04b4 -r 5ced6472ac3c Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 06:35:57 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 06:50:33 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.
 *}