# HG changeset patch
# User wenzelm
# Date 1152872313 -7200
# Node ID 282165caaeaf95bf55715354bcbe5092ed6cf30c
# Parent  20229342ca760c041a9f3a9597470b92298b0696
simp method: depth_limit;

diff -r 20229342ca76 -r 282165caaeaf doc-src/IsarRef/generic.tex
--- 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