# HG changeset patch
# User nipkow
# Date 965215031 -7200
# Node ID 44fefb6e99945939cc1637a96983ddf5f7fa33cd
# Parent  494f8cd34df74ee49b1b3ec1adf2468633346e64
*** empty log message ***

diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/Misc/asm_simp.thy
--- a/doc-src/TutorialI/Misc/asm_simp.thy	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Wed Aug 02 13:17:11 2000 +0200
@@ -33,11 +33,13 @@
 text{*\noindent
 There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
-\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
+\item[\isa{(no_asm)}]\indexbold{*no_asm}
+ means that assumptions are completely ignored.
+\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
+ means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified
-but are not
+\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
+ means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
 Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Wed Aug 02 13:17:11 2000 +0200
@@ -29,11 +29,13 @@
 \noindent
 There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
-\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
+\item[\isa{(no_asm)}]\indexbold{*no_asm}
+ means that assumptions are completely ignored.
+\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
+ means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified
-but are not
+\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
+ means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
 Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/Misc/document/fakenat.tex
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Wed Aug 02 13:17:11 2000 +0200
@@ -2,8 +2,8 @@
 %
 \begin{isamarkuptext}%
 \noindent
-The type \isaindexbold{nat} of natural numbers is predefined and
-behaves like%
+The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
+numbers is predefined and behaves like%
 \end{isamarkuptext}%
 \isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}%
 %%% Local Variables:
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/Misc/fakenat.thy
--- a/doc-src/TutorialI/Misc/fakenat.thy	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/Misc/fakenat.thy	Wed Aug 02 13:17:11 2000 +0200
@@ -3,8 +3,8 @@
 (*>*)
 
 text{*\noindent
-The type \isaindexbold{nat} of natural numbers is predefined and
-behaves like
+The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
+numbers is predefined and behaves like
 *}
 
 datatype nat = "0" | Suc nat
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 02 13:17:11 2000 +0200
@@ -220,8 +220,9 @@
 text{*
 \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
 
-After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
-\isacommand{oops}) we start a new proof:
+After abandoning the above proof attempt\indexbold{abandon
+proof}\indexbold{proof!abandon} (at the shell level type
+\isacommand{oops}\indexbold{*oops}) we start a new proof:
 *}
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 02 13:17:11 2000 +0200
@@ -209,8 +209,9 @@
 \begin{isamarkuptext}%
 \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
 
-After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
-\isacommand{oops}) we start a new proof:%
+After abandoning the above proof attempt\indexbold{abandon
+proof}\indexbold{proof!abandon} (at the shell level type
+\isacommand{oops}\indexbold{*oops}) we start a new proof:%
 \end{isamarkuptext}%
 \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
 \begin{isamarkuptxt}%
diff -r 494f8cd34df7 -r 44fefb6e9994 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Aug 02 11:30:38 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Wed Aug 02 13:17:11 2000 +0200
@@ -125,7 +125,8 @@
   \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   
   If you suddenly discover that you need to modify a parent theory of your
-  current theory you must first abandon your current theory (at the shell
+  current theory you must first abandon your current theory\indexbold{abandon
+  theory}\indexbold{theory!abandon} (at the shell
   level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
   been modified you go back to your original theory. When its first line
   \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
@@ -316,21 +317,22 @@
 see~\S\ref{nat-numerals}.
 
 \begin{warn}
-  The operations \ttindexboldpos{+}{$HOL2arithfun},
-  \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
-  \isaindexbold{min}, \isaindexbold{max},
+  The constant \ttindexbold{0} and the operations
+  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
+  \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},
   \indexboldpos{\isasymle}{$HOL2arithrel} and
   \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   not just for natural numbers but at other types as well (see
-  \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x},
-  there is nothing to indicate that you are talking about natural numbers.
-  Hence Isabelle can only infer that \isa{x} and \isa{y} are of some
-  arbitrary type where \isa{+} is declared. As a consequence, you will be
-  unable to prove the goal (although it may take you some time to realize
-  what has happened if \texttt{show_types} is not set).  In this particular
-  example, you need to include an explicit type constraint, for example
-  \isa{x+y = y+(x::nat)}.  If there is enough contextual information this may
-  not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}.
+  \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
+  is nothing to indicate that you are talking about natural numbers.  Hence
+  Isabelle can only infer that \isa{x} is of some arbitrary type where
+  \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
+  prove the goal (although it may take you some time to realize what has
+  happened if \texttt{show_types} is not set).  In this particular example,
+  you need to include an explicit type constraint, for example \isa{x+0 =
+    (x::nat)}.  If there is enough contextual information this may not be
+  necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because
+  \isa{Suc} is not overloaded.
 \end{warn}
 
 Simple arithmetic goals are proved automatically by both \isa{auto}