author | blanchet |
Fri, 18 Oct 2013 15:00:40 +0200 | |
changeset 54152 | f15bd1f81220 |
parent 54151 | 71dc4e6c001c |
child 54153 | 67487a607ce2 |
--- 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. *}