# HG changeset patch
# User berghofe
# Date 1033476328 -7200
# Node ID 1430360d97823549b4f52b45472afad161d8fb84
# Parent  7316f30c37b20c4e43729e7737eb80fd3a76c2b8
Documented new "asm_lr" option for simp.

diff -r 7316f30c37b2 -r 1430360d9782 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Oct 01 14:44:43 2002 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Oct 01 14:45:28 2002 +0200
@@ -657,12 +657,15 @@
 \railalias{noasmuse}{no\_asm\_use}
 \railterm{noasmuse}
 
+\railalias{asmlr}{asm\_lr}
+\railterm{asmlr}
+
 \indexouternonterm{simpmod}
 \begin{rail}
   ('simp' | simpall) ('!' ?) opt? (simpmod *)
   ;
 
-  opt: '(' (noasm | noasmsimp | noasmuse) ')'
+  opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'
   ;
   simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
     'split' (() | 'add' | 'del')) ':' thmrefs
@@ -706,6 +709,9 @@
 \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}).
 
 \medskip