--- a/doc-src/TutorialI/Recdef/termination.thy Tue May 07 14:28:34 2002 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Tue May 07 15:03:50 2002 +0200
@@ -39,7 +39,7 @@
proved). Because \isacommand{recdef}'s termination prover involves
simplification, we include in our second attempt a hint: the
\attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
-simplification rule. *}
+simplification rule.\cmmdx{hints} *}
(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
recdef qs "measure length"