document limitations
authorblanchet
Mon, 24 Oct 2016 20:32:02 +0200
changeset 64383 b9d4efb43fd9
parent 64382 2a75139b5931
child 64384 f8c1c12d6af5
document limitations
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>