# HG changeset patch
# User wenzelm
# Date 975968437 -3600
# Node ID 38e626f7dfa919ec565069db63f2868bc2721ce1
# Parent  f2d9f4fd370b120ba23a329c608569259d53057a
diagnostic commands: comment;

diff -r f2d9f4fd370b -r 38e626f7dfa9 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Dec 04 23:18:24 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Mon Dec 04 23:20:37 2000 +0100
@@ -1189,13 +1189,13 @@
 \begin{rail}
   'pr' modes? nat? (',' nat)?
   ;
-  'thm' modes? thmrefs
+  'thm' modes? thmrefs comment?
   ;
-  'term' modes? term
+  'term' modes? term comment?
   ;
-  'prop' modes? prop
+  'prop' modes? prop comment?
   ;
-  'typ' modes? type
+  'typ' modes? type comment?
   ;
 
   modes: '(' (name + ) ')'