# HG changeset patch
# User wenzelm
# Date 960069460 -7200
# Node ID bb7622789bf243ddd48222b9c16d6f60043417f2
# Parent  2962c80230e3f483109c7f4db03a53542be20f79
'next', '{', '}': comment;

diff -r 2962c80230e3 -r bb7622789bf2 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Jun 03 23:57:04 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Sat Jun 03 23:57:40 2000 +0200
@@ -924,6 +924,21 @@
   \EN & : & \isartrans{proof(state)}{proof(state)} \\
 \end{matharray}
 
+\railalias{lbrace}{\ttlbrace}
+\railterm{lbrace}
+
+\railalias{rbrace}{\ttrbrace}
+\railterm{rbrace}
+
+\begin{rail}
+  'next' comment?
+  ;
+  lbrace comment?
+  ;
+  rbrace comment?
+  ;
+\end{rail}
+
 While Isar is inherently block-structured, opening and closing blocks is
 mostly handled rather casually, with little explicit user-intervention.  Any
 local goal statement automatically opens \emph{two} blocks, which are closed