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