--- a/doc-src/IsarRef/generic.tex Thu Jul 13 17:39:56 2006 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Jul 14 12:18:33 2006 +0200
@@ -914,27 +914,12 @@
simp_all & : & \isarmeth \\
\end{matharray}
-\railalias{simpall}{simp\_all}
-\railterm{simpall}
-
-\railalias{noasm}{no\_asm}
-\railterm{noasm}
-
-\railalias{noasmsimp}{no\_asm\_simp}
-\railterm{noasmsimp}
-
-\railalias{noasmuse}{no\_asm\_use}
-\railterm{noasmuse}
-
-\railalias{asmlr}{asm\_lr}
-\railterm{asmlr}
-
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | simpall) ('!' ?) opt? (simpmod *)
+ ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
;
- opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'
+ opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
;
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
'split' (() | 'add' | 'del')) ':' thmrefs
@@ -972,15 +957,17 @@
Additional Simplifier options may be specified to tune the behavior further
(mostly for unstructured scripts with many accidental local facts):
-``$(no_asm)$'' means assumptions are ignored completely (cf.\
+``$(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.\
+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{full_simp_tac}).
-For compatibility reasons, there is also an option ``$(asm_lr)$'',
-which means that an assumption is only used for simplifying assumptions
-which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}).
+conclusion (cf.\ \texttt{full_simp_tac}). For compatibility reasons, there is
+also an option ``$(asm_lr)$'', which means that an assumption is only used for
+simplifying assumptions which are to the right of it (cf.\
+\texttt{asm_lr_simp_tac}). Giving an option ``$(depth_limit: n)$'' limits the
+number of recursive invocations of the simplifier during conditional
+rewriting.
\medskip