diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Tue Jul 17 13:46:21 2001 +0200
@@ -5,7 +5,7 @@
 subsection{*Case Expressions*}
 
 text{*\label{sec:case-expressions}
-HOL also features \isaindexbold{case}-expressions for analyzing
+HOL also features \sdx{case}-expressions for analyzing
 elements of a datatype. For example,
 @{term[display]"case xs of [] => 1 | y#ys => y"}
 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
@@ -47,10 +47,10 @@
 \indexbold{induction!structural}
 \indexbold{case distinction}
 Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
+simplification. Only induction is invoked by hand via \methdx{induct_tac},
 which works for any datatype. In some cases, induction is overkill and a case
 distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:
+by \methdx{case_tac}. A trivial example:
 *}
 
 lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";