| changeset 46999 | 1c3c185bab4e |
| parent 45600 | 1bbbac9a0cb0 |
| child 47114 | 7c9e31ffcd9e |
--- a/doc-src/IsarRef/Thy/Spec.thy Sat Mar 17 17:58:40 2012 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Sat Mar 17 22:46:19 2012 +0100 @@ -103,10 +103,10 @@ \end{matharray} @{rail " - @@{command context} @{syntax name} @'begin' + @@{command context} @{syntax nameref} @'begin' ; - @{syntax_def target}: '(' @'in' @{syntax name} ')' + @{syntax_def target}: '(' @'in' @{syntax nameref} ')' "} \begin{description}