diff -r 17684cf64fda -r ca86e84ce200 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Thu Oct 03 10:34:51 2002 +0200 +++ b/doc-src/IsarRef/conversion.tex Fri Oct 04 09:56:48 2002 +0200 @@ -358,6 +358,7 @@ \texttt{Simp_tac 1} & & simp~(no_asm) \\ \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\ \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\ + \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\ \end{matharray} Isar also provides separate method modifier syntax for augmenting the