Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarImplementation/Thy/ML.thy
changeset 42665 e4c5c7ffceea
parent 42517 b68e1c27709a
child 46262 912b42e64fde 
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue May 03 21:29:25 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue May 03 21:40:14 2011 +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 '}' | '\<lbrace>' | '\<rbrace>'
   "}
 
   Here @{syntax nameref} and @{syntax args} are regular outer syntax
isabelle