--- a/doc-src/TutorialI/Recdef/termination.thy Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Tue Jul 17 15:07:36 2001 +0200
@@ -41,8 +41,9 @@
text{*\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
-we include with our second attempt the hint to use @{thm[source]termi_lem} as
-a simplification rule:\indexbold{*recdef_simp}
+we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
+says to use @{thm[source]termi_lem} as
+a simplification rule.
*}
consts g :: "nat\<times>nat \<Rightarrow> nat";