
diff -r 2fda15dd1e0f -r 13660d5f6a77 doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Fri Apr 22 12:43:53 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Fri Apr 22 18:08:57 1994 +0200
@@ -9,9 +9,8 @@
 the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
   CTT}) form a richer world for mathematical reasoning and, again, many
 examples are in the literature.  Higher-order logic~({\tt HOL}) is
-Isabelle's most sophisticated logic, because its types and functions are
-identified with those of the meta-logic; this may cause difficulties for
-beginners.
+Isabelle's most sophisticated logic because its types and functions are
+identified with those of the meta-logic.
 
 Choose a logic that you already understand.  Isabelle is a proof
 tool, not a teaching tool; if you do not know how to do a particular proof
@@ -113,10 +112,10 @@
   \Var{P}\bimp \Var{Q}  & \equiv & 
                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
 \end{eqnarray*}
-\index{meta-rewriting}
+\index{meta-rewriting}%
 Isabelle permits {\bf meta-level rewriting} using definitions such as
 these.  {\bf Unfolding} replaces every instance
-of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$.  For
+of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
 \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
 {\bf Folding} a definition replaces occurrences of the right-hand side by
@@ -124,7 +123,7 @@
 
 When you define new concepts, you should derive rules asserting their
 abstract properties, and then forget their definitions.  This supports
-modularity: if you later change the definitions, without affecting their
+modularity: if you later change the definitions without affecting their
 abstract properties, then most of your proofs will carry through without
 change.  Indiscriminate unfolding makes a subgoal grow exponentially,
 becoming unreadable.
@@ -336,7 +335,7 @@
 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
 classes      {\it class declarations}
 default      {\it sort}
-types        {\it type declarations}
+types        {\it type declarations and synonyms}
 arities      {\it arity declarations}
 consts       {\it constant declarations}
 rules        {\it rule declarations}
@@ -361,30 +360,30 @@
 or more other theories, inheriting their types, constants, syntax, etc.
 The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
 
-Each theory definition must reside in a separate file, whose name is
-determined as follows: the theory name, say {\tt ListFn}, is converted to
-lower case and {\tt.thy} is appended, yielding the filename {\tt
-  listfn.thy}.  Isabelle uses this convention to locate the file containing
-a given theory; \ttindexbold{use_thy} automatically loads a theory's
-parents before loading the theory itself.
+Each theory definition must reside in a separate file, whose name is the
+theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
+on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
+file containing a given theory; \ttindexbold{use_thy} automatically loads a
+theory's parents before loading the theory itself.
 
-Calling \ttindexbold{use_thy}~{\tt"}{\it T\/}{\tt"} reads a theory from the
-file {\it t}{\tt.thy}, writes the corresponding {\ML} code to the file
-{\tt.}{\it t}{\tt.thy.ML}, reads the latter file, and deletes it if no errors
-occured.  This declares the {\ML} structure~$T$, which contains a component
+Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
+file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
+{\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
+occurred.  This declares the {\ML} structure~$T$, which contains a component
 {\tt thy} denoting the new theory, a component for each rule, and everything
 declared in {\it ML code}.
 
 Errors may arise during the translation to {\ML} (say, a misspelled keyword)
 or during creation of the new theory (say, a type error in a rule).  But if
-all goes well, {\tt use_thy} will finally read the file {\it t}{\tt.ML}, if
+all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
 it exists.  This file typically begins with the {\ML} declaration {\tt
 open}~$T$ and contains proofs that refer to the components of~$T$.
 
 When a theory file is modified, many theories may have to be reloaded.
 Isabelle records the modification times and dependencies of theory files.
-See the {\em Reference Manual\/}
-\iflabelundefined{sec:reloading-theories}{}{(\S\ref{sec:reloading-theories})}
+See 
+\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
+                 {\S\ref{sec:reloading-theories}}
 for more details.
 
 
@@ -491,7 +490,7 @@
 
 A type constructor may be overloaded (subject to certain conditions) by
 appearing in several arity declarations.  For instance, the function type
-constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order
+constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
 logic, it is declared also to have arity $(term,term)term$.
 
 Theory {\tt List} declares the 1-place type constructor $list$, gives
@@ -521,7 +520,7 @@
 translator passes them verbatim to the {\ML} output file.
 \end{warn}
 
-\subsection{Type synonyms}\indexbold{types!synonyms}
+\subsection{Type synonyms}\indexbold{type 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
 and are fairly self explanatory:
@@ -791,7 +790,7 @@
 \end{ttbox}
 
 \subsection{Proving some recursion equations}
-File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the
+File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
 natural numbers.  As a trivial example, let us derive recursion equations
 for \verb$+$.  Here is the zero case:
 \begin{ttbox}
@@ -969,7 +968,7 @@
 number is exponential in the size of the formula.
 
 \subsection{Proving that addition is associative}
-Let us invoke the induction rule properly properly, using~{\tt
+Let us invoke the induction rule properly, using~{\tt
   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
 simplification tactics, which are described in 
 \iflabelundefined{simp-chap}%
@@ -981,7 +980,7 @@
 perhaps proving it.  For efficiency, the rewrite rules must be
 packaged into a {\bf simplification set},\index{simplification sets} 
 or {\bf simpset}.  We take the standard simpset for first-order logic and
-insert the equations for~{\tt add} proved in the previous section, namely
+insert the equations proved in the previous section, namely
 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
 \begin{ttbox}
 val add_ss = FOL_ss addrews [add_0, add_Suc];
@@ -1003,7 +1002,7 @@
 \end{ttbox}
 The base case holds easily; both sides reduce to $m+n$.  The
 tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
-set, applying the rewrite rules for~{\tt +}:
+set, applying the rewrite rules for addition:
 \begin{ttbox}
 by (simp_tac add_ss 1);
 {\out Level 2}
@@ -1011,7 +1010,7 @@
 {\out  1. !!x. x + m + n = x + (m + n) ==>}
 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
 \end{ttbox}
-The inductive step requires rewriting by the equations for~{\tt add}
+The inductive step requires rewriting by the equations for addition
 together the induction hypothesis, which is also an equation.  The
 tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
 useful assumptions:
@@ -1028,7 +1027,7 @@
 \index{Prolog interpreter|bold}
 To demonstrate the power of tacticals, let us construct a Prolog
 interpreter and execute programs involving lists.\footnote{To run these
-examples, see the file {\tt FOL/ex/prolog.ML}.} The Prolog program
+examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program
 consists of a theory.  We declare a type constructor for lists, with an
 arity declaration to say that $(\tau)list$ is of class~$term$
 provided~$\tau$ is:
@@ -1199,7 +1198,7 @@
 {\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
 \end{ttbox}
 The tactic has failed to find a solution!  It reached a dead end at
-subgoal~1: there is no~$\Var{x1}$ such that [] appended with~$[\Var{x1}]$
+subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
 equals~$[a,b,c]$.  Backtracking explores other outcomes.
 \begin{ttbox}
 back();




