changeset 13111 | 2d6782e71702 |
parent 11705 | ac8ca15c556c |
child 17914 | 99ead7a7eb42 |
--- a/doc-src/TutorialI/Advanced/WFrec.thy Tue May 07 14:28:34 2002 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Tue May 07 15:03:50 2002 +0200 @@ -107,7 +107,7 @@ text{*\noindent Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a -crucial hint to our definition: +crucial hint\cmmdx{hints} to our definition: *} (*<*) consts g :: "nat \<Rightarrow> nat"