# 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 \<Rightarrow> 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\<times>nat \<Rightarrow> 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}