1.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Nov 29 10:22:38 2000 +0100
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Nov 29 13:44:26 2000 +0100
     1.3 @@ -142,7 +142,8 @@
     1.4  
     1.5  HOL-Types: HOL $(LOG)/HOL-Types.gz
     1.6  
     1.7 -$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \
     1.8 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Pairs.thy \
     1.9 +  Types/Typedef.thy \
    1.10    Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.11    Types/Overloading.thy Types/Axioms.thy
    1.12  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
    1.13 @@ -155,7 +156,6 @@
    1.14  $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
    1.15    Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
    1.16    Misc/prime_def.thy Misc/case_exprs.thy \
    1.17 -  Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \
    1.18    Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
    1.19  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
    1.20  	@rm -f tutorial.dvi

     2.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 10:22:38 2000 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 13:44:26 2000 +0100
     2.3 @@ -4,9 +4,6 @@
     2.4  use_thy "case_exprs";
     2.5  use_thy "fakenat";
     2.6  use_thy "natsum";
     2.7 -use_thy "arith1";
     2.8 -use_thy "arith2";
     2.9 -use_thy "arith3";
    2.10  use_thy "pairs";
    2.11  use_thy "types";
    2.12  use_thy "prime_def";

     3.1 --- a/doc-src/TutorialI/Misc/arith1.thy	Wed Nov 29 10:22:38 2000 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,8 +0,0 @@
     3.4 -(*<*)
     3.5 -theory arith1 = Main:;
     3.6 -(*>*)
     3.7 -lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
     3.8 -(**)(*<*)
     3.9 -by(auto);
    3.10 -end
    3.11 -(*>*)

     4.1 --- a/doc-src/TutorialI/Misc/arith2.thy	Wed Nov 29 10:22:38 2000 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,9 +0,0 @@
     4.4 -(*<*)
     4.5 -theory arith2 = Main:;
     4.6 -(*>*)
     4.7 -lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
     4.8 -apply(arith);
     4.9 -(**)(*<*)
    4.10 -done
    4.11 -end
    4.12 -(*>*)

     5.1 --- a/doc-src/TutorialI/Misc/arith3.thy	Wed Nov 29 10:22:38 2000 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,8 +0,0 @@
     5.4 -(*<*)
     5.5 -theory arith3 = Main:;
     5.6 -(*>*)
     5.7 -lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1";
     5.8 -(**)(*<*)
     5.9 -oops;
    5.10 -end
    5.11 -(*>*)

     6.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex	Wed Nov 29 10:22:38 2000 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,9 +0,0 @@
     6.4 -%
     6.5 -\begin{isabellebody}%
     6.6 -\def\isabellecontext{arith{\isadigit{1}}}%
     6.7 -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
     6.8 -\end{isabellebody}%
     6.9 -%%% Local Variables:
    6.10 -%%% mode: latex
    6.11 -%%% TeX-master: "root"
    6.12 -%%% End:

     7.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex	Wed Nov 29 10:22:38 2000 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,10 +0,0 @@
     7.4 -%
     7.5 -\begin{isabellebody}%
     7.6 -\def\isabellecontext{arith{\isadigit{2}}}%
     7.7 -\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
     7.8 -\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
     7.9 -\end{isabellebody}%
    7.10 -%%% Local Variables:
    7.11 -%%% mode: latex
    7.12 -%%% TeX-master: "root"
    7.13 -%%% End:

     8.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex	Wed Nov 29 10:22:38 2000 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,9 +0,0 @@
     8.4 -%
     8.5 -\begin{isabellebody}%
     8.6 -\def\isabellecontext{arith{\isadigit{3}}}%
     8.7 -\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
     8.8 -\end{isabellebody}%
     8.9 -%%% Local Variables:
    8.10 -%%% mode: latex
    8.11 -%%% TeX-master: "root"
    8.12 -%%% End:

     9.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Nov 29 10:22:38 2000 +0100
     9.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Nov 29 13:44:26 2000 +0100
     9.3 @@ -20,7 +20,80 @@
     9.4  \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
     9.5  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
     9.6  \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
     9.7 -\isacommand{done}\isanewline
     9.8 +\isacommand{done}%
     9.9 +\begin{isamarkuptext}%
    9.10 +\newcommand{\mystar}{*%
    9.11 +}
    9.12 +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
    9.13 +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
    9.14 +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
    9.15 +\isaindexbold{max} are predefined, as are the relations
    9.16 +\indexboldpos{\isasymle}{$HOL2arithrel} and
    9.17 +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
    9.18 +\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
    9.19 +Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
    9.20 +and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
    9.21 +\isa{Suc}-expressions. If you need the full set of numerals,
    9.22 +see~\S\ref{nat-numerals}.
    9.23 +
    9.24 +\begin{warn}
    9.25 +  The constant \ttindexbold{0} and the operations
    9.26 +  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
    9.27 +  \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
    9.28 +  \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
    9.29 +  \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
    9.30 +  not just for natural numbers but at other types as well (see
    9.31 +  \S\ref{sec:overloading}). For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
    9.32 +  there is nothing to indicate that you are talking about natural numbers.
    9.33 +  Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
    9.34 +  \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
    9.35 +  to prove the goal (although it may take you some time to realize what has
    9.36 +  happened if \isa{show{\isacharunderscore}types} is not set).  In this particular example,
    9.37 +  you need to include an explicit type constraint, for example
    9.38 +  \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}. If there is enough contextual information this
    9.39 +  may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
    9.40 +  \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
    9.41 +\end{warn}
    9.42 +
    9.43 +Simple arithmetic goals are proved automatically by both \isa{auto} and the
    9.44 +simplification methods introduced in \S\ref{sec:Simplification}.  For
    9.45 +example,%
    9.46 +\end{isamarkuptext}%
    9.47 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    9.48 +\begin{isamarkuptext}%
    9.49 +\noindent
    9.50 +is proved automatically. The main restriction is that only addition is taken
    9.51 +into account; other arithmetic operations and quantified formulae are ignored.
    9.52 +
    9.53 +For more complex goals, there is the special method \isaindexbold{arith}
    9.54 +(which attacks the first subgoal). It proves arithmetic goals involving the
    9.55 +usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
    9.56 +\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
    9.57 +\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. For example,%
    9.58 +\end{isamarkuptext}%
    9.59 +\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    9.60 +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}%
    9.61 +\begin{isamarkuptext}%
    9.62 +\noindent
    9.63 +succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
    9.64 +\end{isamarkuptext}%
    9.65 +\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
    9.66 +\begin{isamarkuptext}%
    9.67 +\noindent
    9.68 +is not even proved by \isa{arith} because the proof relies essentially
    9.69 +on properties of multiplication.
    9.70 +
    9.71 +\begin{warn}
    9.72 +  The running time of \isa{arith} is exponential in the number of occurrences
    9.73 +  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
    9.74 +  \isaindexbold{max} because they are first eliminated by case distinctions.
    9.75 +
    9.76 +  \isa{arith} is incomplete even for the restricted class of formulae
    9.77 +  described above (known as ``linear arithmetic''). If divisibility plays a
    9.78 +  role, it may fail to prove a valid formula, for example
    9.79 +  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
    9.80 +\end{warn}%
    9.81 +\end{isamarkuptext}%
    9.82  \end{isabellebody}%
    9.83  %%% Local Variables:
    9.84  %%% mode: latex

    10.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Wed Nov 29 10:22:38 2000 +0100
    10.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Wed Nov 29 13:44:26 2000 +0100
    10.3 @@ -3,25 +3,28 @@
    10.4  \def\isabellecontext{pairs}%
    10.5  %
    10.6  \begin{isamarkuptext}%
    10.7 +\label{sec:pairs}\indexbold{product type}
    10.8 +\index{pair|see{product type}}\index{tuple|see{product type}}
    10.9  HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   10.10 -\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
   10.11 -$\tau@i$. The components of a pair are extracted by \isa{fst} and
   10.12 -\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   10.13 +\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
   10.14 +$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
   10.15 +\isaindexbold{snd}:
   10.16 + \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   10.17  are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   10.18  for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   10.19  $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
   10.20  \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   10.21  
   10.22 -It is possible to use (nested) tuples as patterns in abstractions, for
   10.23 -example \isa{\isasymlambda(x,y,z).x+y+z} and
   10.24 -\isa{\isasymlambda((x,y),z).x+y+z}.
   10.25 -In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
   10.26 -most variable binding constructs. Typical examples are
   10.27 -\begin{quote}
   10.28 -\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
   10.29 -\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
   10.30 -\end{quote}
   10.31 -Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
   10.32 +There is also the type \isaindexbold{unit}, which contains exactly one
   10.33 +element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
   10.34 +as a degenerate Cartesian product of 0 types.
   10.35 +
   10.36 +Note that products, like type \isa{nat}, are datatypes, which means
   10.37 +in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to
   10.38 +products (see \S\ref{sec:products}).
   10.39 +
   10.40 +Instead of tuples with many components (where ``many'' is not much above 2),
   10.41 +it is far preferable to use records (see \S\ref{sec:records}).%
   10.42  \end{isamarkuptext}%
   10.43  \end{isabellebody}%
   10.44  %%% Local Variables:

    11.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Nov 29 10:22:38 2000 +0100
    11.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Nov 29 13:44:26 2000 +0100
    11.3 @@ -7,7 +7,7 @@
    11.4  primitive recursion, for example
    11.5  *}
    11.6  
    11.7 -consts sum :: "nat \\<Rightarrow> nat";
    11.8 +consts sum :: "nat \<Rightarrow> nat";
    11.9  primrec "sum 0 = 0"
   11.10          "sum (Suc n) = Suc n + sum n";
   11.11  
   11.12 @@ -20,6 +20,85 @@
   11.13  apply(auto);
   11.14  done
   11.15  
   11.16 +text{*\newcommand{\mystar}{*%
   11.17 +}
   11.18 +The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
   11.19 +\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
   11.20 +\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
   11.21 +\isaindexbold{max} are predefined, as are the relations
   11.22 +\indexboldpos{\isasymle}{$HOL2arithrel} and
   11.23 +\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
   11.24 +\isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
   11.25 +Isabelle does not prove this completely automatically. Note that @{term 1}
   11.26 +and @{term 2} are available as abbreviations for the corresponding
   11.27 +@{term Suc}-expressions. If you need the full set of numerals,
   11.28 +see~\S\ref{nat-numerals}.
   11.29 +
   11.30 +\begin{warn}
   11.31 +  The constant \ttindexbold{0} and the operations
   11.32 +  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   11.33 +  \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
   11.34 +  \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   11.35 +  \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   11.36 +  not just for natural numbers but at other types as well (see
   11.37 +  \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"},
   11.38 +  there is nothing to indicate that you are talking about natural numbers.
   11.39 +  Hence Isabelle can only infer that @{term x} is of some arbitrary type where
   11.40 +  @{term 0} and @{text"+"} are declared. As a consequence, you will be unable
   11.41 +  to prove the goal (although it may take you some time to realize what has
   11.42 +  happened if @{text show_types} is not set).  In this particular example,
   11.43 +  you need to include an explicit type constraint, for example
   11.44 +  @{prop"x+0 = (x::nat)"}. If there is enough contextual information this
   11.45 +  may not be necessary: @{prop"Suc x = x"} automatically implies
   11.46 +  @{text"x::nat"} because @{term Suc} is not overloaded.
   11.47 +\end{warn}
   11.48 +
   11.49 +Simple arithmetic goals are proved automatically by both @{term auto} and the
   11.50 +simplification methods introduced in \S\ref{sec:Simplification}.  For
   11.51 +example,
   11.52 +*}
   11.53 +
   11.54 +lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
   11.55 +(*<*)by(auto)(*>*)
   11.56 +
   11.57 +text{*\noindent
   11.58 +is proved automatically. The main restriction is that only addition is taken
   11.59 +into account; other arithmetic operations and quantified formulae are ignored.
   11.60 +
   11.61 +For more complex goals, there is the special method \isaindexbold{arith}
   11.62 +(which attacks the first subgoal). It proves arithmetic goals involving the
   11.63 +usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
   11.64 +@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
   11.65 +@{text"+"}, @{text"-"}, @{term min} and @{term max}. For example,
   11.66 +*}
   11.67 +
   11.68 +lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
   11.69 +apply(arith)
   11.70 +(*<*)done(*>*)
   11.71 +
   11.72 +text{*\noindent
   11.73 +succeeds because @{term"k*k"} can be treated as atomic. In contrast,
   11.74 +*}
   11.75 +
   11.76 +lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"
   11.77 +(*<*)oops(*>*)
   11.78 +
   11.79 +text{*\noindent
   11.80 +is not even proved by @{text arith} because the proof relies essentially
   11.81 +on properties of multiplication.
   11.82 +
   11.83 +\begin{warn}
   11.84 +  The running time of @{text arith} is exponential in the number of occurrences
   11.85 +  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   11.86 +  \isaindexbold{max} because they are first eliminated by case distinctions.
   11.87 +
   11.88 +  \isa{arith} is incomplete even for the restricted class of formulae
   11.89 +  described above (known as ``linear arithmetic''). If divisibility plays a
   11.90 +  role, it may fail to prove a valid formula, for example
   11.91 +  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
   11.92 +\end{warn}
   11.93 +*}
   11.94 +
   11.95  (*<*)
   11.96  end
   11.97  (*>*)

    12.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Wed Nov 29 10:22:38 2000 +0100
    12.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Wed Nov 29 13:44:26 2000 +0100
    12.3 @@ -1,26 +1,28 @@
    12.4  (*<*)
    12.5  theory pairs = Main:;
    12.6  (*>*)
    12.7 -text{*
    12.8 +text{*\label{sec:pairs}\indexbold{product type}
    12.9 +\index{pair|see{product type}}\index{tuple|see{product type}}
   12.10  HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   12.11 -\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
   12.12 -$\tau@i$. The components of a pair are extracted by @{term"fst"} and
   12.13 -@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   12.14 +\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
   12.15 +$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
   12.16 +\isaindexbold{snd}:
   12.17 + \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   12.18  are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   12.19  for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   12.20  $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
   12.21  \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   12.22  
   12.23 -It is possible to use (nested) tuples as patterns in abstractions, for
   12.24 -example \isa{\isasymlambda(x,y,z).x+y+z} and
   12.25 -\isa{\isasymlambda((x,y),z).x+y+z}.
   12.26 -In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
   12.27 -most variable binding constructs. Typical examples are
   12.28 -\begin{quote}
   12.29 -@{term"let (x,y) = f z in (y,x)"}\\
   12.30 -@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
   12.31 -\end{quote}
   12.32 -Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
   12.33 +There is also the type \isaindexbold{unit}, which contains exactly one
   12.34 +element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
   12.35 +as a degenerate Cartesian product of 0 types.
   12.36 +
   12.37 +Note that products, like type @{typ nat}, are datatypes, which means
   12.38 +in particular that @{text induct_tac} and @{text case_tac} are applicable to
   12.39 +products (see \S\ref{sec:products}).
   12.40 +
   12.41 +Instead of tuples with many components (where ``many'' is not much above 2),
   12.42 +it is far preferable to use records (see \S\ref{sec:records}).
   12.43  *}
   12.44  (*<*)
   12.45  end

    13.1 --- a/doc-src/TutorialI/Types/Overloading0.thy	Wed Nov 29 10:22:38 2000 +0100
    13.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy	Wed Nov 29 13:44:26 2000 +0100
    13.3 @@ -25,18 +25,19 @@
    13.4  Isabelle will not complain because the three definitions do not overlap: no
    13.5  two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
    13.6  common instance. What is more, the recursion in @{thm[source]inverse_pair} is
    13.7 -benign because the type of @{term inverse} becomes smaller: on the left it is
    13.8 -@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
    13.9 -'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do
   13.10 -intentionally define @{term inverse} only at instances of its declared type
   13.11 -@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
   13.12 +benign because the type of @{term[source]inverse} becomes smaller: on the
   13.13 +left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
   13.14 +@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"(overloaded)"} tells Isabelle that
   13.15 +the definitions do intentionally define @{term[source]inverse} only at
   13.16 +instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
   13.17 +warnings to that effect.
   13.18  
   13.19  However, there is nothing to prevent the user from forming terms such as
   13.20 -@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
   13.21 -although we never defined inverse on lists. We hasten to say that there is
   13.22 -nothing wrong with such terms and theorems. But it would be nice if we could
   13.23 -prevent their formation, simply because it is very likely that the user did
   13.24 -not mean to write what he did. Thus he had better not waste his time pursuing
   13.25 -it further. This requires the use of type classes.
   13.26 +@{term[source]"inverse []"} and proving theorems as @{prop[source]"inverse []
   13.27 += inverse []"}, although we never defined inverse on lists. We hasten to say
   13.28 +that there is nothing wrong with such terms and theorems. But it would be
   13.29 +nice if we could prevent their formation, simply because it is very likely
   13.30 +that the user did not mean to write what he did. Thus he had better not waste
   13.31 +his time pursuing it further. This requires the use of type classes.
   13.32  *}
   13.33  (*<*)end(*>*)

    14.1 --- a/doc-src/TutorialI/Types/ROOT.ML	Wed Nov 29 10:22:38 2000 +0100
    14.2 +++ b/doc-src/TutorialI/Types/ROOT.ML	Wed Nov 29 13:44:26 2000 +0100
    14.3 @@ -1,4 +1,5 @@
    14.4  use "../settings.ML";
    14.5 +use_thy "Pairs";
    14.6  use_thy "Typedef";
    14.7  use_thy "Overloading0";
    14.8  use_thy "Overloading2";

    15.1 --- a/doc-src/TutorialI/Types/document/Overloading0.tex	Wed Nov 29 10:22:38 2000 +0100
    15.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Wed Nov 29 13:44:26 2000 +0100
    15.3 @@ -29,18 +29,19 @@
    15.4  Isabelle will not complain because the three definitions do not overlap: no
    15.5  two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
    15.6  common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
    15.7 -benign because the type of \isa{Overloading{\isadigit{0}}{\isachardot}inverse} becomes smaller: on the left it is
    15.8 -\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
    15.9 -intentionally define \isa{Overloading{\isadigit{0}}{\isachardot}inverse} only at instances of its declared type
   15.10 -\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
   15.11 +benign because the type of \isa{inverse} becomes smaller: on the
   15.12 +left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
   15.13 +\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that
   15.14 +the definitions do intentionally define \isa{inverse} only at
   15.15 +instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
   15.16 +warnings to that effect.
   15.17  
   15.18  However, there is nothing to prevent the user from forming terms such as
   15.19 -\isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}},
   15.20 -although we never defined inverse on lists. We hasten to say that there is
   15.21 -nothing wrong with such terms and theorems. But it would be nice if we could
   15.22 -prevent their formation, simply because it is very likely that the user did
   15.23 -not mean to write what he did. Thus he had better not waste his time pursuing
   15.24 -it further. This requires the use of type classes.%
   15.25 +\isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}} and proving theorems as \isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}, although we never defined inverse on lists. We hasten to say
   15.26 +that there is nothing wrong with such terms and theorems. But it would be
   15.27 +nice if we could prevent their formation, simply because it is very likely
   15.28 +that the user did not mean to write what he did. Thus he had better not waste
   15.29 +his time pursuing it further. This requires the use of type classes.%
   15.30  \end{isamarkuptext}%
   15.31  \end{isabellebody}%
   15.32  %%% Local Variables:

    16.1 --- a/doc-src/TutorialI/Types/types.tex	Wed Nov 29 10:22:38 2000 +0100
    16.2 +++ b/doc-src/TutorialI/Types/types.tex	Wed Nov 29 13:44:26 2000 +0100
    16.3 @@ -6,25 +6,23 @@
    16.4  advanced material:
    16.5  \begin{itemize}
    16.6  \item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
    16.7 -  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
    16.8 -  about them.
    16.9 +  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
   16.10 +  reason about them.
   16.11  \item Introducing your own types: how to introduce your own new types that
   16.12 -  cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}).
   16.13 +  cannot be constructed with any of the basic methods
   16.14 +  ({\S}\ref{sec:adv-typedef}).
   16.15  \item Type classes: how to specify and reason about axiomatic collections of
   16.16    types ({\S}\ref{sec:axclass}).
   16.17  \end{itemize}
   16.18  
   16.19 -\section{Basic types}
   16.20 -
   16.21 -\subsection{Numbers}
   16.22 +\section{Numbers}
   16.23  \label{sec:numbers}
   16.24  
   16.25 -\subsection{Pairs}
   16.26 -\label{sec:products}
   16.27 +\input{Types/document/Pairs}
   16.28  % Check refs to this section to see what is expected of it.
   16.29  % Mention type unit
   16.30  
   16.31 -\subsection{Records}
   16.32 +\section{Records}
   16.33  \label{sec:records}
   16.34  
   16.35  \input{Types/document/Typedef}

    17.1 --- a/doc-src/TutorialI/appendix.tex	Wed Nov 29 10:22:38 2000 +0100
    17.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Nov 29 13:44:26 2000 +0100
    17.3 @@ -61,7 +61,7 @@
    17.4  \indexboldpos{\isasymle}{$HOL2arithrel}&
    17.5  \ttindexboldpos{<=}{$HOL2arithrel}&
    17.6  \verb$\<le>$\\
    17.7 -\indexboldpos{\isasymtimes}{$IsaFun}&
    17.8 +\indexboldpos{\isasymtimes}{$Isatype}&
    17.9  \ttindexboldpos{*}{$HOL2arithfun} &
   17.10  \verb$\<times>$\\
   17.11  \indexboldpos{\isasymin}{$HOL3Set0a}&

    18.1 --- a/doc-src/TutorialI/basics.tex	Wed Nov 29 10:22:38 2000 +0100
    18.2 +++ b/doc-src/TutorialI/basics.tex	Wed Nov 29 13:44:26 2000 +0100
    18.3 @@ -102,7 +102,7 @@
    18.4    which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
    18.5      \isasymFun~$\tau$}.
    18.6  \item[type variables,]\indexbold{type variable}\indexbold{variable!type}
    18.7 -  denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
    18.8 +  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise
    18.9    to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   18.10    function.
   18.11  \end{description}
   18.12 @@ -183,10 +183,10 @@
   18.13  Despite type inference, it is sometimes necessary to attach explicit
   18.14  \textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
   18.15  \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
   18.16 -\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
   18.17 +\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
   18.18  in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
   18.19  \isa{(x < y)::nat}. The main reason for type constraints are overloaded
   18.20 -functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for
   18.21 +functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
   18.22  a full discussion of overloading.
   18.23  
   18.24  \begin{warn}

    19.1 --- a/doc-src/TutorialI/fp.tex	Wed Nov 29 10:22:38 2000 +0100
    19.2 +++ b/doc-src/TutorialI/fp.tex	Wed Nov 29 13:44:26 2000 +0100
    19.3 @@ -186,7 +186,7 @@
    19.4  primitive recursive function definitions.
    19.5  
    19.6  Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
    19.7 -the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
    19.8 +the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
    19.9  just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
   19.10    1}.  In general, \isaindexbold{size} returns \isa{0} for all constructors
   19.11  that do not have an argument of type $t$, and for all other constructors
   19.12 @@ -209,7 +209,7 @@
   19.13  becomes smaller with every recursive call. There must be exactly one equation
   19.14  for each constructor.  Their order is immaterial.
   19.15  A more general method for defining total recursive functions is introduced in
   19.16 -\S\ref{sec:recdef}.
   19.17 +{\S}\ref{sec:recdef}.
   19.18  
   19.19  \begin{exercise}\label{ex:Tree}
   19.20  \input{Misc/document/Tree.tex}%
   19.21 @@ -220,7 +220,7 @@
   19.22  \begin{warn}
   19.23    Induction is only allowed on free (or \isasymAnd-bound) variables that
   19.24    should not occur among the assumptions of the subgoal; see
   19.25 -  \S\ref{sec:ind-var-in-prems} for details. Case distinction
   19.26 +  {\S}\ref{sec:ind-var-in-prems} for details. Case distinction
   19.27    (\isa{case_tac}) works for arbitrary terms, which need to be
   19.28    quoted if they are non-atomic.
   19.29  \end{warn}
   19.30 @@ -238,94 +238,12 @@
   19.31  \input{Misc/document/fakenat.tex}
   19.32  \input{Misc/document/natsum.tex}
   19.33  
   19.34 -The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
   19.35 -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
   19.36 -\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
   19.37 -\isaindexbold{max} are predefined, as are the relations
   19.38 -\indexboldpos{\isasymle}{$HOL2arithrel} and
   19.39 -\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
   19.40 -\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although
   19.41 -Isabelle does not prove this completely automatically. Note that \isa{1} and
   19.42 -\isa{2} are available as abbreviations for the corresponding
   19.43 -\isa{Suc}-expressions. If you need the full set of numerals,
   19.44 -see~\S\ref{nat-numerals}.
   19.45 -
   19.46 -\begin{warn}
   19.47 -  The constant \ttindexbold{0} and the operations
   19.48 -  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   19.49 -  \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},
   19.50 -  \indexboldpos{\isasymle}{$HOL2arithrel} and
   19.51 -  \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   19.52 -  not just for natural numbers but at other types as well (see
   19.53 -  \S\ref{sec:overloading}). For example, given the goal \isa{x+0 = x}, there
   19.54 -  is nothing to indicate that you are talking about natural numbers.  Hence
   19.55 -  Isabelle can only infer that \isa{x} is of some arbitrary type where
   19.56 -  \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
   19.57 -  prove the goal (although it may take you some time to realize what has
   19.58 -  happened if \texttt{show_types} is not set).  In this particular example,
   19.59 -  you need to include an explicit type constraint, for example \isa{x+0 =
   19.60 -    (x::nat)}.  If there is enough contextual information this may not be
   19.61 -  necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because
   19.62 -  \isa{Suc} is not overloaded.
   19.63 -\end{warn}
   19.64 -
   19.65 -Simple arithmetic goals are proved automatically by both \isa{auto}
   19.66 -and the simplification methods introduced in \S\ref{sec:Simplification}.  For
   19.67 -example,
   19.68 -
   19.69 -\input{Misc/document/arith1.tex}%
   19.70 -is proved automatically. The main restriction is that only addition is taken
   19.71 -into account; other arithmetic operations and quantified formulae are ignored.
   19.72 -
   19.73 -For more complex goals, there is the special method
   19.74 -\isaindexbold{arith} (which attacks the first subgoal). It proves
   19.75 -arithmetic goals involving the usual logical connectives (\isasymnot,
   19.76 -\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and
   19.77 -the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example,
   19.78 -
   19.79 -\input{Misc/document/arith2.tex}%
   19.80 -succeeds because \isa{k*k} can be treated as atomic.
   19.81 -In contrast,
   19.82 -
   19.83 -\input{Misc/document/arith3.tex}%
   19.84 -is not even proved by \isa{arith} because the proof relies essentially
   19.85 -on properties of multiplication.
   19.86 -
   19.87 -\begin{warn}
   19.88 -  The running time of \isa{arith} is exponential in the number of occurrences
   19.89 -  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   19.90 -  \isaindexbold{max} because they are first eliminated by case distinctions.
   19.91 -
   19.92 -  \isa{arith} is incomplete even for the restricted class of formulae
   19.93 -  described above (known as ``linear arithmetic''). If divisibility plays a
   19.94 -  role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
   19.95 -  Fortunately, such examples are rare in practice.
   19.96 -\end{warn}
   19.97 -
   19.98  \index{arithmetic|)}
   19.99  
  19.100  
  19.101  \subsection{Pairs}
  19.102  \input{Misc/document/pairs.tex}
  19.103  
  19.104 -%FIXME move stuff below into section on proofs about products?
  19.105 -\begin{warn}
  19.106 -  Abstraction over pairs and tuples is merely a convenient shorthand for a
  19.107 -  more complex internal representation.  Thus the internal and external form
  19.108 -  of a term may differ, which can affect proofs. If you want to avoid this
  19.109 -  complication, use \isa{fst} and \isa{snd}, i.e.\ write
  19.110 -  \isa{\isasymlambda{}p.~fst p + snd p} instead of
  19.111 -  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{sec:products} for
  19.112 -  theorem proving with tuple patterns.
  19.113 -\end{warn}
  19.114 -
  19.115 -Note that products, like type \isa{nat}, are datatypes, which means
  19.116 -in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
  19.117 -products (see \S\ref{sec:products}).
  19.118 -
  19.119 -Instead of tuples with many components (where ``many'' is not much above 2),
  19.120 -it is far preferable to use records (see \S\ref{sec:records}).
  19.121 -
  19.122  \section{Definitions}
  19.123  \label{sec:Definitions}
  19.124  
  19.125 @@ -346,7 +264,7 @@
  19.126  
  19.127  Note that pattern-matching is not allowed, i.e.\ each definition must be of
  19.128  the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
  19.129 -Section~\S\ref{sec:Simplification} explains how definitions are used
  19.130 +Section~{\S}\ref{sec:Simplification} explains how definitions are used
  19.131  in proofs.
  19.132  
  19.133  \input{Misc/document/prime_def.tex}
  19.134 @@ -357,15 +275,15 @@
  19.135  The purpose of this chapter is to deepen the reader's understanding of the
  19.136  concepts encountered so far and to introduce advanced forms of datatypes and
  19.137  recursive functions. The first two sections give a structured presentation of
  19.138 -theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
  19.139 -important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
  19.140 +theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
  19.141 +important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can
  19.142  be skipped by readers less interested in proofs. They are followed by a case
  19.143 -study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
  19.144 +study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
  19.145  datatypes, including those involving function spaces, are covered in
  19.146 -\S\ref{sec:advanced-datatypes}, which closes with another case study, search
  19.147 +{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search
  19.148  trees (``tries'').  Finally we introduce \isacommand{recdef}, a very general
  19.149  form of recursive function definition which goes well beyond what
  19.150 -\isacommand{primrec} allows (\S\ref{sec:recdef}).
  19.151 +\isacommand{primrec} allows ({\S}\ref{sec:recdef}).
  19.152  
  19.153  
  19.154  \section{Simplification}
  19.155 @@ -382,7 +300,7 @@
  19.156  many other systems. The tool itself is called the \bfindex{simplifier}. The
  19.157  purpose of this section is introduce the many features of the simplifier.
  19.158  Anybody intending to use HOL should read this section. Later on
  19.159 -(\S\ref{sec:simplification-II}) we explain some more advanced features and a
  19.160 +({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
  19.161  little bit of how the simplifier works. The serious student should read that
  19.162  section as well, in particular in order to understand what happened if things
  19.163  do not simplify as expected.
  19.164 @@ -550,7 +468,7 @@
  19.165  recursion need not involve datatypes, and termination is proved by showing
  19.166  that the arguments of all recursive calls are smaller in a suitable (user
  19.167  supplied) sense. In this section we ristrict ourselves to measure functions;
  19.168 -more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}.
  19.169 +more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
  19.170  
  19.171  \subsection{Defining recursive functions}
  19.172