# HG changeset patch
# User wenzelm
# Date 957558287 -7200
# Node ID 6ec0c8f9d68dc3832689519d464417caaf7b6476
# Parent  d0eae42f6d12a31924efd4095a7493cc55b10c1b
improved syntax of method options (no_asm) etc;

diff -r d0eae42f6d12 -r 6ec0c8f9d68d doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri May 05 22:24:03 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri May 05 22:24:47 2000 +0200
@@ -392,7 +392,7 @@
   ('simp' | simpall) ('!' ?) opt? (simpmod * )
   ;
 
-  opt: (noasm | noasmsimp | noasmuse) ':'
+  opt: '(' (noasm | noasmsimp | noasmuse) ')'
   ;
   simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   ;
@@ -425,11 +425,11 @@
 should be used with some care, though.
 
 Additional Simplifier options may be specified to tune the behavior even
-further: $no_asm$ means assumptions are ignored completely (cf.\ 
-\texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the
+further: $(no_asm)$ means assumptions are ignored completely (cf.\ 
+\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
 simplification of the conclusion but are not themselves simplified (cf.\ 
-\texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but
-are not used in the simplification of each other or the conclusion (cf.
+\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
+but are not used in the simplification of each other or the conclusion (cf.
 \texttt{full_simp_tac}).
 
 \medskip
diff -r d0eae42f6d12 -r 6ec0c8f9d68d doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Fri May 05 22:24:03 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Fri May 05 22:24:47 2000 +0200
@@ -232,9 +232,9 @@
 about large specifications.
 
 \begin{rail}
-  'cases' ('simplified' ':')? term? rule?  ;
+  'cases' ('(' 'simplified' ')')? term? rule?  ;
 
-  'induct' ('stripped' ':')? (insts * 'and') rule?
+  'induct' ('(' 'stripped' ')')? (insts * 'and') rule?
   ;
 
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref