# HG changeset patch
# User lcp
# Date 765472185 -7200
# Node ID 994dbab40849cbee1a5b615887866d6b1345a96b
# Parent  eee166d4a532229c792da0d7955e054861cb6fd8
modifications towards final draft

diff -r eee166d4a532 -r 994dbab40849 doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Wed Mar 30 17:31:18 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Mon Apr 04 17:09:45 1994 +0200
@@ -36,15 +36,15 @@
 \label{deriving-example}
 \index{examples!of deriving rules}
 
-The subgoal module supports the derivation of rules.  The \ttindex{goal}
-command, when supplied a goal of the form $\List{\theta@1; \ldots;
-\theta@k} \Imp \phi$, creates $\phi\Imp\phi$ as the initial proof state and
-returns a list consisting of the theorems 
-${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.  These meta-assumptions are
-also recorded internally, allowing \ttindex{result} to discharge them in the
-original order.
+The subgoal module supports the derivation of rules, as discussed in
+\S\ref{deriving}.  The \ttindex{goal} command, when supplied a goal of the
+form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
+as the initial proof state and returns a list consisting of the theorems
+${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.  These meta-assumptions
+are also recorded internally, allowing \ttindex{result} to discharge them
+in the original order.
 
-Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle.
+Let us derive $\conj$ elimination using Isabelle.
 Until now, calling \ttindex{goal} has returned an empty list, which we have
 thrown away.  In this example, the list contains the two premises of the
 rule.  We bind them to the \ML\ identifiers {\tt major} and {\tt
@@ -353,7 +353,7 @@
 The {\ML} section contains code to perform arbitrary syntactic
 transformations.  The main declaration forms are discussed below.
 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
-  appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}.
+  appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
 
 All the declaration parts can be omitted.  In the simplest case, $T$ is
 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
@@ -518,28 +518,26 @@
 translator passes them verbatim to the {\ML} output file.
 \end{warn}
 
-\subsection{Type synonyms}
-\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}}
-
+\subsection{Type synonyms}\indexbold{types!synonyms}
 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
-to those found in ML. Such synonyms are defined in the type declaration part
+to those found in \ML.  Such synonyms are defined in the type declaration part
 and are fairly self explanatory:
 \begin{ttbox}
-types gate = "[o,o] => o"
-      'a pred = "'a => o"
+types gate       = "[o,o] => o"
+      'a pred    = "'a => o"
       ('a,'b)nuf = "'b => 'a"
 \end{ttbox}
 Type declarations and synonyms can be mixed arbitrarily:
 \begin{ttbox}
 types nat
       'a stream = "nat => 'a"
-      signal = "nat stream"
+      signal    = "nat stream"
       'a list
 \end{ttbox}
-A synonym is merely an abbreviation for some existing type expression. Hence
-synonyms may not be recursive! Internally all synonyms are fully expanded. As
-a consequence Isabelle output never contains synonyms. Their main purpose is
-to improve the readability of theories. Synonyms can be used just like any
+A synonym is merely an abbreviation for some existing type expression.  Hence
+synonyms may not be recursive!  Internally all synonyms are fully expanded.  As
+a consequence Isabelle output never contains synonyms.  Their main purpose is
+to improve the readability of theories.  Synonyms can be used just like any
 other type:
 \begin{ttbox}
 consts and,or :: "gate"
@@ -641,7 +639,7 @@
         \(id\) < \(c@1\), \ldots, \(c@k\)
 \end{ttbox}
 Type classes allow constants to be overloaded.  As suggested in
-\S\ref{polymorphic}, let us define the class $arith$ of ``arithmetic''
+\S\ref{polymorphic}, let us define the class $arith$ of arithmetic
 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
 \alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
 $term$ and add the three polymorphic constants of this class.
@@ -699,7 +697,7 @@
 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
 Let us introduce the Peano axioms for mathematical induction and the
 freeness of $0$ and~$Suc$:
-\[ \vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
+\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
  \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
 \]
 \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
@@ -752,7 +750,9 @@
 \index{examples!of theories}
 Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
 which contains only classical logic with no natural numbers.  We declare
-the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:
+the 0-place type constructor $nat$ and the associated constants.  Note that
+the constant~0 requires a mixfix annotation because~0 is not a legal
+identifier, and could not otherwise be written in terms:
 \begin{ttbox}
 Nat = FOL +
 types   nat
@@ -835,7 +835,7 @@
 \end{description}
 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
-with no leading question marks!! --- and $e@1$, \ldots, $e@n$ are
+with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
 expressions giving their instantiations.  The expressions are type-checked
 in the context of a particular subgoal: free variables receive the same
 types as they have in the subgoal, and parameters may appear.  Type