doc-src/TutorialI/Recdef/termination.thy
changeset 10654 458068404143
parent 10522 ed3964d1f1a4
child 10795 9e888d60d3e5
     1.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  text{*\noindent
     1.5  Because \isacommand{recdef}'s termination prover involves simplification,
     1.6  we include with our second attempt the hint to use @{thm[source]termi_lem} as
     1.7 -a simplification rule:
     1.8 +a simplification rule:\indexbold{*recdef_simp}
     1.9  *}
    1.10  
    1.11  consts g :: "nat\<times>nat \<Rightarrow> nat";