# HG changeset patch
# User wenzelm
# Date 967924041 -7200
# Node ID 221388d5696d8b3fac77bc460d93ef95df60e02c
# Parent  038b018f86f5676d8a2141c07dc165ecafc63d47
tuned rail;

diff -r 038b018f86f5 -r 221388d5696d doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Sat Sep 02 21:47:08 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Sat Sep 02 21:47:21 2000 +0200
@@ -214,9 +214,9 @@
 about large specifications.
 
 \begin{rail}
-  'cases' ('(simplified)')? ('(open)')? \\ (insts * 'and') rule?  ;
+  'cases' ('(' 'simplified' ')')? ('(' 'open' ')')? \\ (insts * 'and') rule?  ;
 
-  'induct' ('(stripped)')? ('(open)')? \\ (insts * 'and') rule?
+  'induct' ('(' 'stripped' ')')? ('(' 'open' ')')? \\ (insts * 'and') rule?
   ;
 
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref