| changeset 48605 | e777363440d6 |
| parent 48604 | f651323139f0 |
| child 48650 | 47330b712f8f |
--- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:38:45 2012 +0200 +++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 15:31:00 2012 +0200 @@ -60,7 +60,9 @@ ; options: @'options' opts ; - opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']' + opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' + ; + value: @{syntax name} | @{syntax real} ; theories: @'theories' opts? ( @{syntax name} + ) ;