src/Doc/Corec/Corec.thy
 changeset 64383 b9d4efb43fd9 parent 64380 4b22e1268779 child 64384 f8c1c12d6af5
equal inserted replaced
64382:2a75139b5931 64383:b9d4efb43fd9
   937 \emph{There is no mechanism for registering custom plugins.}
   937 \emph{There is no mechanism for registering custom plugins.}
   938
   938
   939 \item
   939 \item
   940 \emph{The package does not interact well with locales.}
   940 \emph{The package does not interact well with locales.}
   941
   941

   942 \item

   943 \emph{The undocumented @{text corecUU_transfer} theorem is not as polymorphic as

   944 it could be.}

   945

   946 \item

   947 \emph{All type variables occurring in the arguments of a friendly function must occur

   948 as direct arguments of the type constructor of the resulting type.}

   949
   942 \end{enumerate}
   950 \end{enumerate}
   943 \<close>
   951 \<close>
   944
   952
   945 end
   953 end