| changeset 42813 | 6c841fa92fa2 |
| parent 42705 | 528a2ba8fa74 |
| child 42936 | 48a0a9db3453 |
--- a/doc-src/IsarRef/Thy/Spec.thy Sun May 15 16:40:24 2011 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Sun May 15 17:06:35 2011 +0200 @@ -859,7 +859,7 @@ (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} ; - @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text} + @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? "} \begin{description}