# HG changeset patch
# User blanchet
# Date 1477333922 -7200
# Node ID b9d4efb43fd9d714217702445de82b2a32290ea6
# Parent  2a75139b59314be64b20b4cfeb22c63836f58381
document limitations

diff -r 2a75139b5931 -r b9d4efb43fd9 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Mon Oct 24 20:32:02 2016 +0200
+++ b/src/Doc/Corec/Corec.thy	Mon Oct 24 20:32:02 2016 +0200
@@ -939,6 +939,14 @@
 \item
 \emph{The package does not interact well with locales.}
 
+\item
+\emph{The undocumented @{text corecUU_transfer} theorem is not as polymorphic as
+it could be.}
+
+\item
+\emph{All type variables occurring in the arguments of a friendly function must occur
+as direct arguments of the type constructor of the resulting type.}
+
 \end{enumerate}
 \<close>