1.1 --- a/doc-src/Intro/advanced.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -293,7 +293,7 @@
     1.4  \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
     1.5      Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
     1.6  object-logics may add further theory sections, for example
     1.7 -\texttt{typedef}, \texttt{datatype} in \HOL.
     1.8 +\texttt{typedef}, \texttt{datatype} in HOL.
     1.9  
    1.10  All the declaration parts can be omitted or repeated and may appear in
    1.11  any order, except that the {\ML} section must be last (after the {\tt
    1.12 @@ -302,7 +302,7 @@
    1.13  theories, inheriting their types, constants, syntax, etc.  The theory
    1.14  \thydx{Pure} contains nothing but Isabelle's meta-logic.  The variant
    1.15  \thydx{CPure} offers the more usual higher-order function application
    1.16 -syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure.
    1.17 +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
    1.18  
    1.19  Each theory definition must reside in a separate file, whose name is
    1.20  the theory's with {\tt.thy} appended.  Calling
    1.21 @@ -964,12 +964,11 @@
    1.22  
    1.23  \index{simplification}\index{examples!of simplification} 
    1.24  
    1.25 -Isabelle's simplification tactics repeatedly apply equations to a
    1.26 -subgoal, perhaps proving it.  For efficiency, the rewrite rules must
    1.27 -be packaged into a {\bf simplification set},\index{simplification
    1.28 -  sets} or {\bf simpset}.  We augment the implicit simpset of {\FOL}
    1.29 -with the equations proved in the previous section, namely $0+n=n$ and
    1.30 -$\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
    1.31 +Isabelle's simplification tactics repeatedly apply equations to a subgoal,
    1.32 +perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
    1.33 +{\bf simplification set},\index{simplification sets} or {\bf simpset}.  We
    1.34 +augment the implicit simpset of FOL with the equations proved in the previous
    1.35 +section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
    1.36  \begin{ttbox}
    1.37  Addsimps [add_0, add_Suc];
    1.38  \end{ttbox}