--- 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