generalized limitation in documentation
authorblanchet
Thu, 16 Jul 2015 17:25:44 +0200
changeset 60736 c4bc0691860b
parent 60735 cf291b55f3d1
child 60737 685b169d0611
generalized limitation in documentation
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:25:44 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:25:44 2015 +0200
@@ -3186,8 +3186,8 @@
 processed more efficiently.
 
 \item
-\emph{Locally fixed types cannot be used in (co)datatype specifications.}
-This limitation can be circumvented by adding type arguments to the local
+\emph{Locally fixed types and terms cannot be used in type specifications.}
+The limitation on types can be circumvented by adding type arguments to the local
 (co)datatypes to abstract over the locally fixed types.
 
 \item