1.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy	Tue Jul 17 13:46:21 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy	Tue Jul 17 15:07:36 2001 +0200
     1.3 @@ -105,8 +105,8 @@
     1.4  
     1.5  text{*\noindent
     1.6  
     1.7 -Armed with this lemma, we can append a crucial hint to our definition:
     1.8 -\indexbold{*recdef_wf}
     1.9 +Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
    1.10 +crucial hint to our definition:
    1.11  *}
    1.12  (*<*)
    1.13  consts g :: "nat \<Rightarrow> nat"

     2.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Tue Jul 17 13:46:21 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Tue Jul 17 15:07:36 2001 +0200
     2.3 @@ -101,8 +101,8 @@
     2.4  \begin{isamarkuptext}%
     2.5  \noindent
     2.6  
     2.7 -Armed with this lemma, we can append a crucial hint to our definition:
     2.8 -\indexbold{*recdef_wf}%
     2.9 +Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
    2.10 +crucial hint to our definition:%
    2.11  \end{isamarkuptext}%
    2.12  {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
    2.13  \begin{isamarkuptext}%

     3.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Jul 17 13:46:21 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Jul 17 15:07:36 2001 +0200
     3.3 @@ -38,8 +38,9 @@
     3.4  \begin{isamarkuptext}%
     3.5  \noindent
     3.6  Because \isacommand{recdef}'s termination prover involves simplification,
     3.7 -we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
     3.8 -a simplification rule:\indexbold{*recdef_simp}%
     3.9 +we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
    3.10 +says to use \isa{termi{\isacharunderscore}lem} as
    3.11 +a simplification rule.%
    3.12  \end{isamarkuptext}%
    3.13  \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    3.14  \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline

     4.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Tue Jul 17 13:46:21 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Tue Jul 17 15:07:36 2001 +0200
     4.3 @@ -41,8 +41,9 @@
     4.4  
     4.5  text{*\noindent
     4.6  Because \isacommand{recdef}'s termination prover involves simplification,
     4.7 -we include with our second attempt the hint to use @{thm[source]termi_lem} as
     4.8 -a simplification rule:\indexbold{*recdef_simp}
     4.9 +we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
    4.10 +says to use @{thm[source]termi_lem} as
    4.11 +a simplification rule.  
    4.12  *}
    4.13  
    4.14  consts g :: "nat\<times>nat \<Rightarrow> nat";

     5.1 --- a/doc-src/TutorialI/tutorial.ind	Tue Jul 17 13:46:21 2001 +0200
     5.2 +++ b/doc-src/TutorialI/tutorial.ind	Tue Jul 17 15:07:36 2001 +0200
     5.3 @@ -450,8 +450,8 @@
     5.4  		\hyperpage{98}, \hyperpage{160--168}
     5.5      \subitem and numeric literals, \hyperpage{132}
     5.6    \item \isa {recdef_cong} (attribute), \hyperpage{164}
     5.7 -  \item \isa {recdef_simp}, \bold{47}
     5.8 -  \item \isa {recdef_wf}, \bold{162}
     5.9 +  \item \isa {recdef_simp} (attribute), \hyperpage{47}
    5.10 +  \item \isa {recdef_wf} (attribute), \hyperpage{162}
    5.11    \item \isacommand {record} (command), \hyperpage{140}
    5.12    \item \isa {record_split} (method), \hyperpage{143}
    5.13    \item records, \hyperpage{140--144}