# HG changeset patch # User paulson # Date 995375256 -7200 # Node ID 30da2f5eaf57e88bde0ef79f8ca75846c501ac58 # Parent 332347b9b942fedd3f49a8a4dce518f51509f823 tidying the index diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Advanced/WFrec.thy --- a/doc-src/TutorialI/Advanced/WFrec.thy Tue Jul 17 13:46:21 2001 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Tue Jul 17 15:07:36 2001 +0200 @@ -105,8 +105,8 @@ text{*\noindent -Armed with this lemma, we can append a crucial hint to our definition: -\indexbold{*recdef_wf} +Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a +crucial hint to our definition: *} (*<*) consts g :: "nat \ nat" diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Jul 17 13:46:21 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Jul 17 15:07:36 2001 +0200 @@ -101,8 +101,8 @@ \begin{isamarkuptext}% \noindent -Armed with this lemma, we can append a crucial hint to our definition: -\indexbold{*recdef_wf}% +Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a +crucial hint to our definition:% \end{isamarkuptext}% {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% \begin{isamarkuptext}% diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Jul 17 13:46:21 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Jul 17 15:07:36 2001 +0200 @@ -38,8 +38,9 @@ \begin{isamarkuptext}% \noindent Because \isacommand{recdef}'s termination prover involves simplification, -we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as -a simplification rule:\indexbold{*recdef_simp}% +we include in our second attempt a hint: the \attrdx{recdef_simp} attribute +says to use \isa{termi{\isacharunderscore}lem} as +a simplification rule.% \end{isamarkuptext}% \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Recdef/termination.thy --- a/doc-src/TutorialI/Recdef/termination.thy Tue Jul 17 13:46:21 2001 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Tue Jul 17 15:07:36 2001 +0200 @@ -41,8 +41,9 @@ 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:\indexbold{*recdef_simp} +we include in our second attempt a hint: the \attrdx{recdef_simp} attribute +says to use @{thm[source]termi_lem} as +a simplification rule. *} consts g :: "nat\nat \ nat"; diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/tutorial.ind --- a/doc-src/TutorialI/tutorial.ind Tue Jul 17 13:46:21 2001 +0200 +++ b/doc-src/TutorialI/tutorial.ind Tue Jul 17 15:07:36 2001 +0200 @@ -450,8 +450,8 @@ \hyperpage{98}, \hyperpage{160--168} \subitem and numeric literals, \hyperpage{132} \item \isa {recdef_cong} (attribute), \hyperpage{164} - \item \isa {recdef_simp}, \bold{47} - \item \isa {recdef_wf}, \bold{162} + \item \isa {recdef_simp} (attribute), \hyperpage{47} + \item \isa {recdef_wf} (attribute), \hyperpage{162} \item \isacommand {record} (command), \hyperpage{140} \item \isa {record_split} (method), \hyperpage{143} \item records, \hyperpage{140--144}