| changeset 10795 | 9e888d60d3e5 |
| parent 10654 | 458068404143 |
| child 10841 | 2fb8089ab6cd |
--- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Jan 05 18:32:57 2001 +0100 @@ -79,7 +79,7 @@ by simp; text{*\noindent -and should have appended the following hint to our above definition: +and should have appended the following hint to our definition above: \indexbold{*recdef_wf} *} (*<*)