| changeset 10654 | 458068404143 |
| parent 10522 | ed3964d1f1a4 |
| child 10795 | 9e888d60d3e5 |
--- a/doc-src/TutorialI/Recdef/termination.thy Wed Dec 13 09:32:55 2000 +0100 +++ b/doc-src/TutorialI/Recdef/termination.thy Wed Dec 13 09:39:53 2000 +0100 @@ -42,7 +42,7 @@ 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: +a simplification rule:\indexbold{*recdef_simp} *} consts g :: "nat\<times>nat \<Rightarrow> nat";