# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282200388 -32400
# Node ID 12283a96e85123bc35d38c16952717e0ca15a7b4
# Parent  e96f3efb00320d5063968939c34099aa4d0fc4ea
The type does determine respectfulness, the constant without an instantiated type does not.

diff -r e96f3efb0032 -r 12283a96e851 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Aug 19 15:02:11 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Thu Aug 19 15:46:28 2010 +0900
@@ -720,9 +720,9 @@
   theorems}. However, unlike his quotient package, we might have several
   respectfulness theorems for one constant---he has at most one.
   The reason is that because of our quotient compositions, the types
-  @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
-  And for every instantiation of the types, we might end up with a 
-  corresponding respectfulness theorem.
+  @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
+  And for every instantiation of the types, a corresponding
+  respectfulness theorem is necessary.
 
   Before lifting a theorem, we require the user to discharge
   respectfulness proof obligations. In case of @{text bn}