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