changeset 53167 | 4e7ddd76e632 |
parent 53163 | 7c2b13a53d69 |
child 53709 | 84522727f9d3 |
--- a/src/Doc/IsarImplementation/ML.thy Fri Aug 23 15:04:00 2013 +0200 +++ b/src/Doc/IsarImplementation/ML.thy Fri Aug 23 15:36:54 2013 +0200 @@ -667,7 +667,7 @@ ML is augmented by special syntactic entities of the following form: @{rail " - @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>' + @{syntax_def antiquote}: '@{' nameref args '}' "} Here @{syntax nameref} and @{syntax args} are regular outer syntax