--- a/Quotient-Paper/Paper.thy	Tue Jun 15 06:35:57 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 07:52:42 2010 +0200
@@ -1088,6 +1088,13 @@
     translation according to given quotients).
 
   \end{itemize}
+
+  \medskip
+  \noindent
+  {\bf Acknowledgements:} We would like to thank Peter Homeier for the
+  discussions about the HOL4 quotient package and explaining us its
+  implementation details.
+
 *}