correct (apparently untested) e1698a9578ea
authortraytel
Wed, 17 Feb 2016 15:18:06 +0100
changeset 62331 e923f200bda5
parent 62330 7d0c92d5dd80
child 62332 eeaa2f7b5329
correct (apparently untested) e1698a9578ea
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 15:18:06 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 17 15:18:06 2016 +0100
@@ -3537,7 +3537,7 @@
 \item
 \emph{The \emph{\keyw{primcorec}} command does not allow corecursion under
 @{text "case"}--@{text "of"} for datatypes that are defined without
-discriminators and selectors.
+discriminators and selectors.}
 
 \item
 \emph{There is no way to use an overloaded constant from a syntactic type