# HG changeset patch
# User nipkow
# Date 967651760 -7200
# Node ID a123a64cadebf89b97599dfc4707f3182225aeee
# Parent  f25ac7194f7148567a7f8b8c2b52b9cd0d3a49b6
*** empty log message ***

diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -2,25 +2,29 @@
 theory Itrev = Main:;
 (*>*)
 
-text{* Function \isa{rev} has quadratic worst-case running time
-because it calls function \isa{\at} for each element of the list and
-\isa{\at} is linear in its first argument.  A linear time version of
-\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only \isa{\#}:*}
+text{*
+Function @{term"rev"} has quadratic worst-case running time
+because it calls function @{term"@"} for each element of the list and
+@{term"@"} is linear in its first argument.  A linear time version of
+@{term"rev"} reqires an extra argument where the result is accumulated
+gradually, using only @{name"#"}:
+*}
 
 consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
 primrec
 "itrev []     ys = ys"
 "itrev (x#xs) ys = itrev xs (x#ys)";
 
-text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
+text{*\noindent
+The behaviour of @{term"itrev"} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
 and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+empty. Note that @{term"itrev"} is tail-recursive, i.e.\ it can be
 compiled into a loop.
 
-Naturally, we would like to show that \isa{itrev} does indeed reverse
-its first argument provided the second one is empty: *};
+Naturally, we would like to show that @{term"itrev"} does indeed reverse
+its first argument provided the second one is empty:
+*};
 
 lemma "itrev xs [] = rev xs";
 
@@ -37,47 +41,46 @@
 \end{isabelle}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
-\isa{[]}. The corresponding heuristic:
+@{term"[]"}. The corresponding heuristic:
 \begin{quote}
-{\em 3. Generalize goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
-
-Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
+Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
 just not true---the correct generalization is
 *};
 (*<*)oops;(*>*)
 lemma "itrev xs ys = rev xs @ ys";
 
 txt{*\noindent
-If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
+If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
 @{term"rev xs"}, just as required.
 
 In this particular instance it was easy to guess the right generalization,
 but in more complex situations a good deal of creativity is needed. This is
 the main source of complications in inductive proofs.
 
-Although we now have two variables, only \isa{xs} is suitable for
+Although we now have two variables, only @{term"xs"} is suitable for
 induction, and we repeat our above proof attempt. Unfortunately, we are still
 not there:
 \begin{isabelle}
 ~1.~{\isasymAnd}a~list.\isanewline
 ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
+~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
 \end{isabelle}
 The induction hypothesis is still too weak, but this time it takes no
-intuition to generalize: the problem is that \isa{ys} is fixed throughout
+intuition to generalize: the problem is that @{term"ys"} is fixed throughout
 the subgoal, but the induction hypothesis needs to be applied with
-@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem
-for all \isa{ys} instead of a fixed one:
+@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
+for all @{term"ys"} instead of a fixed one:
 *};
 (*<*)oops;(*>*)
 lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
 
 txt{*\noindent
-This time induction on \isa{xs} followed by simplification succeeds. This
+This time induction on @{term"xs"} followed by simplification succeeds. This
 leads to another heuristic for generalization:
 \begin{quote}
-{\em 4. Generalize goals for induction by universally quantifying all free
+\emph{Generalize goals for induction by universally quantifying all free
 variables {\em(except the induction variable itself!)}.}
 \end{quote}
 This prevents trivial failures like the above and does not change the
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -38,9 +38,8 @@
 hypothesis, is too weak to solve the induction step because of the fixed
 \isa{[]}. The corresponding heuristic:
 \begin{quote}
-{\em 3. Generalize goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
-
 Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
 just not true---the correct generalization is%
 \end{isamarkuptxt}%
@@ -74,7 +73,7 @@
 This time induction on \isa{xs} followed by simplification succeeds. This
 leads to another heuristic for generalization:
 \begin{quote}
-{\em 4. Generalize goals for induction by universally quantifying all free
+\emph{Generalize goals for induction by universally quantifying all free
 variables {\em(except the induction variable itself!)}.}
 \end{quote}
 This prevents trivial failures like the above and does not change the
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -15,9 +15,7 @@
 you needed to reprove many lemmas reminiscent of similar lemmas about
 @{term"rev"}. We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!
+choose exercise~\ref{ex:trev-trev}:
 *}
 (* consts trev  :: "('a,'b)term => ('a,'b)term" *)
 (*<*)
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -1,12 +1,12 @@
 (*<*)
 theory Nested1 = Nested0:;
 (*>*)
-consts trev  :: "('a,'b)term => ('a,'b)term";
+consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
 
 text{*\noindent
 Although the definition of @{term"trev"} is quite natural, we will have
 overcome a minor difficulty in convincing Isabelle of is termination.
-It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+It is precisely this difficulty that is the \textit{raison d'\^etre} of
 this subsection.
 
 Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
@@ -15,30 +15,30 @@
 *};
 
 recdef trev "measure size"
- "trev (Var x) = Var x"
+ "trev (Var x)    = Var x"
  "trev (App f ts) = App f (rev(map trev ts))";
 
-text{*
-FIXME: recdef should complain and generate unprovable termination condition!
-moveto todo
-
+text{*\noindent
 Remember that function @{term"size"} is defined for each \isacommand{datatype}.
-However, the definition does not succeed. Isabelle complains about an unproved termination
-condition
+However, the definition does not succeed. Isabelle complains about an
+unproved termination condition
 \begin{quote}
-@{term[display]"t : set ts --> size t < Suc (term_size ts)"}
+@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
 \end{quote}
-where @{term"set"} returns the set of elements of a list---no special knowledge of sets is
-required in the following.
-First we have to understand why the recursive call of @{term"trev"} underneath @{term"map"} leads
-to the above condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"} will
-apply @{term"trev"} only to elements of @{term"ts"}. Thus the above condition expresses that
-the size of the argument @{term"t : set ts"} of any recursive call of @{term"trev"} is strictly
-less than @{term"size(App f ts) = Suc(term_size ts)"}.
-We will now prove the termination condition and continue with our definition.
-Below we return to the question of how \isacommand{recdef} ``knows'' about @{term"map"}.
+where @{term"set"} returns the set of elements of a list (no special
+knowledge of sets is required in the following) and @{name"term_list_size ::
+term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
+(when @{name"term"} was defined).  First we have to understand why the
+recursive call of @{term"trev"} underneath @{term"map"} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
+will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
+condition expresses that the size of the argument @{term"t : set ts"} of any
+recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
+Suc(term_list_size ts)"}.  We will now prove the termination condition and
+continue with our definition.  Below we return to the question of how
+\isacommand{recdef} ``knows'' about @{term"map"}.
 *};
 
 (*<*)
 end;
-(*>*)
\ No newline at end of file
+(*>*)
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -7,7 +7,7 @@
 The termintion condition is easily proved by induction:
 *};
 
-lemma [simp]: "t \\<in> set ts \\<longrightarrow> size t < Suc(term_size ts)";
+lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)";
 by(induct_tac ts, auto);
 (*<*)
 recdef trev "measure size"
@@ -19,7 +19,7 @@
 applies it automatically and the above definition of @{term"trev"}
 succeeds now. As a reward for our effort, we can now prove the desired
 lemma directly. The key is the fact that we no longer need the verbose
-induction schema for type \isa{term} but the simpler one arising from
+induction schema for type @{name"term"} but the simpler one arising from
 @{term"trev"}:
 *};
 
@@ -38,8 +38,8 @@
 
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend to go through
-the chain of simplification steps in detail, probably with the help of
-\isa{trace\_simp}.
+the chain of simplification steps in detail; you will probably need the help of
+@{name"trace_simp"}.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -50,9 +50,9 @@
 %{term[display]"App f ts"}
 %\end{quote}
 
-The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype}
-because it brings @{term"rev"} into play, about which already know a lot, in particular
-@{prop"rev(rev xs) = xs"}.
+The above definition of @{term"trev"} is superior to the one in
+\S\ref{sec:nested-datatype} because it brings @{term"rev"} into play, about
+which already know a lot, in particular @{prop"rev(rev xs) = xs"}.
 Thus this proof is a good example of an important principle:
 \begin{quote}
 \emph{Chose your definitions carefully\\
@@ -64,9 +64,9 @@
 like @{term"map"}. For a start, if nothing were known about @{term"map"},
 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
-(term_size ts)"}, without any assumption about \isa{t}.  Therefore
+(term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
-\isa{map\_cong}:
+@{name"map_cong"}:
 \begin{quote}
 @{thm[display,margin=50]"map_cong"[no_vars]}
 \end{quote}
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -13,9 +13,7 @@
 you needed to reprove many lemmas reminiscent of similar lemmas about
 \isa{rev}. We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!%
+choose exercise~\ref{ex:trev-trev}:%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -1,11 +1,11 @@
 %
 \begin{isabellebody}%
-\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
+\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Although the definition of \isa{trev} is quite natural, we will have
 overcome a minor difficulty in convincing Isabelle of is termination.
-It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+It is precisely this difficulty that is the \textit{raison d'\^etre} of
 this subsection.
 
 Defining \isa{trev} by \isacommand{recdef} rather than \isacommand{primrec}
@@ -13,31 +13,30 @@
 suggested at the end of \S\ref{sec:nested-datatype}:%
 \end{isamarkuptext}%
 \isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
-\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
+\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
 \ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
-FIXME: recdef should complain and generate unprovable termination condition!
-moveto todo
-
+\noindent
 Remember that function \isa{size} is defined for each \isacommand{datatype}.
-However, the definition does not succeed. Isabelle complains about an unproved termination
-condition
+However, the definition does not succeed. Isabelle complains about an
+unproved termination condition
 \begin{quote}
 
 \begin{isabelle}%
-\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
+\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
 \end{isabelle}%
 
 \end{quote}
-where \isa{set} returns the set of elements of a list---no special knowledge of sets is
-required in the following.
-First we have to understand why the recursive call of \isa{trev} underneath \isa{map} leads
-to the above condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} will
-apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above condition expresses that
-the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any recursive call of \isa{trev} is strictly
-less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}.
-We will now prove the termination condition and continue with our definition.
-Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
+where \isa{set} returns the set of elements of a list (no special
+knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
+(when \isa{term} was defined).  First we have to understand why the
+recursive call of \isa{trev} underneath \isa{map} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
+will apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above
+condition expresses that the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any
+recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}.  We will now prove the termination condition and
+continue with our definition.  Below we return to the question of how
+\isacommand{recdef} ``knows'' about \isa{map}.%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -5,7 +5,7 @@
 \noindent
 The termintion condition is easily proved by induction:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
@@ -36,8 +36,8 @@
 \begin{isamarkuptext}%
 \noindent
 If the proof of the induction step mystifies you, we recommend to go through
-the chain of simplification steps in detail, probably with the help of
-\isa{trace\_simp}.
+the chain of simplification steps in detail; you will probably need the help of
+\isa{trace{\isacharunderscore}simp}.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -48,9 +48,9 @@
 %{term[display]"App f ts"}
 %\end{quote}
 
-The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}
-because it brings \isa{rev} into play, about which already know a lot, in particular
-\isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
+The above definition of \isa{trev} is superior to the one in
+\S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
+which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
 Thus this proof is a good example of an important principle:
 \begin{quote}
 \emph{Chose your definitions carefully\\
@@ -61,9 +61,9 @@
 sensible termination conditions in the presence of higher-order functions
 like \isa{map}. For a start, if nothing were known about \isa{map},
 \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus
-\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.  Therefore
+\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{\mbox{t}}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
-\isa{map\_cong}:
+\isa{map{\isacharunderscore}cong}:
 \begin{quote}
 
 \begin{isabelle}%
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -26,7 +26,7 @@
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
+the recursive call inside the \isa{if} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does
 something else which leads to the same problem: it splits \isa{if}s if the
 condition simplifies to neither \isa{True} nor \isa{False}. For
@@ -59,11 +59,10 @@
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
 
-The most radical solution is to disable the offending
-\isa{split_if} as shown in the section on case splits in
-\S\ref{sec:SimpFeatures}.
-However, we do not recommend this because it means you will often have to
-invoke the rule explicitly when \isa{if} is involved.
+The most radical solution is to disable the offending \\isa{split{\isacharunderscore}if} as
+shown in the section on case splits in \S\ref{sec:Simplification}.  However,
+we do not recommend this because it means you will often have to invoke the
+rule explicitly when \isa{if} is involved.
 
 If possible, the definition should be given by pattern matching on the left
 rather than \isa{if} on the right. In the case of \isa{gcd} the
@@ -76,7 +75,7 @@
 \begin{isamarkuptext}%
 \noindent
 Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+\isa{\mbox{n}\ {\isasymnoteq}\ \isadigit{0}}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A very simple alternative is to replace \isa{if} by \isa{case}, which
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -7,7 +7,7 @@
 equations become simplification rules, just as with
 \isacommand{primrec}. In most cases this works fine, but there is a subtle
 problem that must be mentioned: simplification may not
-terminate because of automatic splitting of \isa{if}.
+terminate because of automatic splitting of @{name"if"}.
 Let us look at an example:
 *}
 
@@ -24,10 +24,10 @@
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
+the recursive call inside the @{name"if"} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does
-something else which leads to the same problem: it splits \isa{if}s if the
-condition simplifies to neither \isa{True} nor \isa{False}. For
+something else which leads to the same problem: it splits @{name"if"}s if the
+condition simplifies to neither @{term"True"} nor @{term"False"}. For
 example, simplification reduces
 \begin{quote}
 @{term[display]"gcd(m,n) = k"}
@@ -41,18 +41,17 @@
 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
 \end{quote}
 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of
+an @{name"if"}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
 
-The most radical solution is to disable the offending
-\isa{split_if} as shown in the section on case splits in
-\S\ref{sec:SimpFeatures}.
-However, we do not recommend this because it means you will often have to
-invoke the rule explicitly when \isa{if} is involved.
+The most radical solution is to disable the offending \@{name"split_if"} as
+shown in the section on case splits in \S\ref{sec:Simplification}.  However,
+we do not recommend this because it means you will often have to invoke the
+rule explicitly when @{name"if"} is involved.
 
 If possible, the definition should be given by pattern matching on the left
-rather than \isa{if} on the right. In the case of \isa{gcd} the
+rather than @{name"if"} on the right. In the case of @{term"gcd"} the
 following alternative definition suggests itself:
 *}
 
@@ -64,11 +63,11 @@
 
 text{*\noindent
 Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+@{prop"n ~= 0"}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
-A very simple alternative is to replace \isa{if} by \isa{case}, which
-is also available for \isa{bool} but is not split automatically:
+A very simple alternative is to replace @{name"if"} by @{name"case"}, which
+is also available for @{typ"bool"} but is not split automatically:
 *}
 
 consts gcd2 :: "nat*nat \\<Rightarrow> nat";
@@ -79,7 +78,7 @@
 In fact, this is probably the neatest solution next to pattern matching.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove
+derived conditional ones. For @{term"gcd"} it means we have to prove
 *}
 
 lemma [simp]: "gcd (m, 0) = m";
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -405,16 +405,12 @@
 
 Simplification is one of the central theorem proving tools in Isabelle and
 many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is twofold: to introduce the many features of the
-simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
-simplifier works (\S\ref{sec:SimpHow}).  Anybody intending to use HOL should
-read \S\ref{sec:SimpFeatures}, and the serious student should read
-\S\ref{sec:SimpHow} as well in order to understand what happened in case
-things do not simplify as expected.
-
-
-\subsection{Using the simplifier}
-\label{sec:SimpFeatures}
+purpose of this section is introduce the many features of the simplifier.
+Anybody intending to use HOL should read this section. Later on
+(\S\ref{sec:simplification-II}) we explain some more advanced features and a
+little bit of how the simplifier works. The serious student should read that
+section as well, in particular in order to understand what happened if things
+do not simplify as expected.
 
 \subsubsection{What is simplification}
 
@@ -572,11 +568,11 @@
 inductive proofs. The first one we have already mentioned in our initial
 example:
 \begin{quote}
-{\em 1. Theorems about recursive functions are proved by induction.}
+\emph{Theorems about recursive functions are proved by induction.}
 \end{quote}
 In case the function has more than one argument
 \begin{quote}
-{\em 2. Do induction on argument number $i$ if the function is defined by
+\emph{Do induction on argument number $i$ if the function is defined by
 recursion in argument number $i$.}
 \end{quote}
 When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
@@ -598,8 +594,8 @@
 side, the simpler \isa{rev} on the right-hand side. This constitutes
 another, albeit weak heuristic that is not restricted to induction:
 \begin{quote}
-  {\em 5. The right-hand side of an equation should (in some sense) be
-    simpler than the left-hand side.}
+  \emph{The right-hand side of an equation should (in some sense) be simpler
+    than the left-hand side.}
 \end{quote}
 The heuristic is tricky to apply because it is not obvious that
 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/tricks.tex
--- a/doc-src/TutorialI/tricks.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/tricks.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -1,6 +1,7 @@
 \chapter{The Tricks of the Trade}
 
 \section{Simplification}
+\label{sec:simplification-II}
 \index{simplification|(}
 
 \subsection{Advanced features}