doc-src/TutorialI/Advanced/WFrec.thy
changeset 10654 458068404143
parent 10545 216388848786
child 10795 9e888d60d3e5
     1.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  functions. Sometimes this can be quite inconvenient or even
     1.5  impossible. Fortunately, \isacommand{recdef} supports much more
     1.6  general definitions. For example, termination of Ackermann's function
     1.7 -can be shown by means of the lexicographic product @{text"<*lex*>"}:
     1.8 +can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
     1.9  *}
    1.10  
    1.11  consts ack :: "nat\<times>nat \<Rightarrow> nat";
    1.12 @@ -80,6 +80,7 @@
    1.13  
    1.14  text{*\noindent
    1.15  and should have appended the following hint to our above definition:
    1.16 +\indexbold{*recdef_wf}
    1.17  *}
    1.18  (*<*)
    1.19  consts g :: "nat \<Rightarrow> nat"
    1.20 @@ -87,5 +88,5 @@
    1.21  "g 0 = 0"
    1.22  "g (Suc n) = g n"
    1.23  (*>*)
    1.24 -(hints recdef_wf add: wf_id)
    1.25 +(hints recdef_wf: wf_id)
    1.26  (*<*)end(*>*)