# HG changeset patch
# User paulson
# Date 995039919 -7200
# Node ID 53a402c10ba9da6b1f2db5bd0fe4533f4b3906eb
# Parent  499435b4084eaa27d9f59e84f0b0fe8b9c6e775f
indexing tweaks

diff -r 499435b4084e -r 53a402c10ba9 doc-src/TutorialI/Misc/document/fakenat.tex
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Fri Jul 13 17:56:05 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Fri Jul 13 17:58:39 2001 +0200
@@ -4,8 +4,8 @@
 %
 \begin{isamarkuptext}%
 \noindent
-The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
-numbers is predefined and behaves like%
+The type \tydx{nat} of natural
+numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.  It  behaves as if it were declared like this:%
 \end{isamarkuptext}%
 \isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
 %%% Local Variables:
diff -r 499435b4084e -r 53a402c10ba9 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 13 17:56:05 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 13 17:58:39 2001 +0200
@@ -38,7 +38,7 @@
 see~\S\ref{sec:numerals}.
 
 \begin{warn}
-  The constant \ttindexbold{0} and the operations
+  The constant \cdx{0} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
   \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
@@ -70,7 +70,7 @@
 is proved automatically. The main restriction is that only addition is taken
 into account; other arithmetic operations and quantified formulae are ignored.
 
-For more complex goals, there is the special method \isaindexbold{arith}
+For more complex goals, there is the special method \methdx{arith}
 (which attacks the first subgoal). It proves arithmetic goals involving the
 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
diff -r 499435b4084e -r 53a402c10ba9 doc-src/TutorialI/Misc/fakenat.thy
--- a/doc-src/TutorialI/Misc/fakenat.thy	Fri Jul 13 17:56:05 2001 +0200
+++ b/doc-src/TutorialI/Misc/fakenat.thy	Fri Jul 13 17:58:39 2001 +0200
@@ -3,8 +3,8 @@
 (*>*)
 
 text{*\noindent
-The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
-numbers is predefined and behaves like
+The type \tydx{nat} of natural
+numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.  It  behaves as if it were declared like this:
 *}
 
 datatype nat = 0 | Suc nat
diff -r 499435b4084e -r 53a402c10ba9 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Fri Jul 13 17:56:05 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Fri Jul 13 17:58:39 2001 +0200
@@ -36,7 +36,7 @@
 see~\S\ref{sec:numerals}.
 
 \begin{warn}
-  The constant \ttindexbold{0} and the operations
+  The constant \cdx{0} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
   \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
@@ -70,7 +70,7 @@
 is proved automatically. The main restriction is that only addition is taken
 into account; other arithmetic operations and quantified formulae are ignored.
 
-For more complex goals, there is the special method \isaindexbold{arith}
+For more complex goals, there is the special method \methdx{arith}
 (which attacks the first subgoal). It proves arithmetic goals involving the
 usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
 @{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},