doc-src/IsarRef/pure.tex
changeset 10584 38e626f7dfa9
parent 10550 93ca45370c59
child 10640 562e20e543b1
--- 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 + ) ')'