| changeset 58725 | 9402a7f15ed5 |
| parent 58724 | e5f809f52f26 |
| child 58868 | c5e1cce7ace3 |
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 20 21:32:54 2014 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 20 21:44:33 2014 +0200 @@ -194,8 +194,7 @@ Note that the syntax of antiquotations may \emph{not} include source comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim - text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim - "*"}@{verbatim "}"}. + text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}. \begin{description}