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