# HG changeset patch
# User wenzelm
# Date 1212928207 -7200
# Node ID 3d79bbdaf2ef8aad65c1312d10601c829b8f6280
# Parent  61cd3f61d3baad8a3b8bdfb2583718294e222242
simp: depth_limit is now a configuration option;

diff -r 61cd3f61d3ba -r 3d79bbdaf2ef doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Sun Jun 08 14:29:36 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sun Jun 08 14:30:07 2008 +0200
@@ -375,7 +375,7 @@
     ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
+    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
     ;
     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       'split' (() | 'add' | 'del')) ':' thmrefs
@@ -429,7 +429,7 @@
   for simplifying assumptions which are to the right of it (cf.\ @{ML
   asm_lr_simp_tac}).
 
-  Giving an option ``@{text "(depth_limit: n)"}'' limits the number of
+  The configuration option @{text "depth_limit"} limits the number of
   recursive invocations of the simplifier during conditional
   rewriting.