src/Doc/Corec/Corec.thy
changeset 64383 b9d4efb43fd9
parent 64380 4b22e1268779
child 64384 f8c1c12d6af5
--- 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>