diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/Misc/asm_simp.thy
--- a/doc-src/TutorialI/Misc/asm_simp.thy	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Wed Aug 02 13:17:11 2000 +0200
@@ -33,11 +33,13 @@
 text{*\noindent
 There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
-\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
+\item[\isa{(no_asm)}]\indexbold{*no_asm}
+ means that assumptions are completely ignored.
+\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
+ means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified
-but are not
+\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
+ means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
 Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above