doc-src/IsarRef/Thy/Document_Preparation.thy
changeset 42617 77d239840285
parent 42596 6c621a9d612a
child 42626 6ac8c55c657e
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 17:06:40 2011 +0200
@@ -185,7 +185,7 @@
     @{syntax_def antiquotation}:
       @@{antiquotation theory} options @{syntax name} |
       @@{antiquotation thm} options styles @{syntax thmrefs} |
-      @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} |
+      @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
       @@{antiquotation prop} options styles @{syntax prop} |
       @@{antiquotation term} options styles @{syntax term} |
       @@{antiquotation term_type} options styles @{syntax term} |
@@ -212,7 +212,7 @@
     styles: '(' (style + ',') ')'
     ;
     style: (@{syntax name} +)
-  "} %% FIXME check lemma
+  "}
 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim