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