equal
deleted
inserted
replaced
373 \indexouternonterm{simpmod} |
373 \indexouternonterm{simpmod} |
374 \begin{rail} |
374 \begin{rail} |
375 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) |
375 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) |
376 ; |
376 ; |
377 |
377 |
378 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')' |
378 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' |
379 ; |
379 ; |
380 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
380 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
381 'split' (() | 'add' | 'del')) ':' thmrefs |
381 'split' (() | 'add' | 'del')) ':' thmrefs |
382 ; |
382 ; |
383 \end{rail} |
383 \end{rail} |
427 full_simp_tac}). For compatibility reasons, there is also an option |
427 full_simp_tac}). For compatibility reasons, there is also an option |
428 ``@{text "(asm_lr)"}'', which means that an assumption is only used |
428 ``@{text "(asm_lr)"}'', which means that an assumption is only used |
429 for simplifying assumptions which are to the right of it (cf.\ @{ML |
429 for simplifying assumptions which are to the right of it (cf.\ @{ML |
430 asm_lr_simp_tac}). |
430 asm_lr_simp_tac}). |
431 |
431 |
432 Giving an option ``@{text "(depth_limit: n)"}'' limits the number of |
432 The configuration option @{text "depth_limit"} limits the number of |
433 recursive invocations of the simplifier during conditional |
433 recursive invocations of the simplifier during conditional |
434 rewriting. |
434 rewriting. |
435 |
435 |
436 \medskip The Splitter package is usually configured to work as part |
436 \medskip The Splitter package is usually configured to work as part |
437 of the Simplifier. The effect of repeatedly applying @{ML |
437 of the Simplifier. The effect of repeatedly applying @{ML |