updated docs
authorblanchet
Fri, 18 Oct 2013 15:00:40 +0200
changeset 54152 f15bd1f81220
parent 54151 71dc4e6c001c
child 54153 67487a607ce2
updated docs
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Oct 18 14:58:02 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Oct 18 15:00:40 2013 +0200
@@ -786,6 +786,10 @@
 
 \end{description}
 \end{indentblock}
+
+\noindent
+In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
+attribute.
 *}