1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sun Jun 08 14:29:36 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sun Jun 08 14:30:07 2008 +0200
     1.3 @@ -375,7 +375,7 @@
     1.4      ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     1.5      ;
     1.6  
     1.7 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
     1.8 +    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
     1.9      ;
    1.10      simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
    1.11        'split' (() | 'add' | 'del')) ':' thmrefs
    1.12 @@ -429,7 +429,7 @@
    1.13    for simplifying assumptions which are to the right of it (cf.\ @{ML
    1.14    asm_lr_simp_tac}).
    1.15  
    1.16 -  Giving an option ``@{text "(depth_limit: n)"}'' limits the number of
    1.17 +  The configuration option @{text "depth_limit"} limits the number of
    1.18    recursive invocations of the simplifier during conditional
    1.19    rewriting.
    1.20