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