# HG changeset patch
# User wenzelm
# Date 862851026 -7200
# Node ID 5396e99c02af7918e577ab1a7a3e893f60af9e66
# Parent  1a5bfa2ab1d1afd861b5e1fa94c0f64b9f18d16f
tuned;

diff -r 1a5bfa2ab1d1 -r 5396e99c02af doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Mon May 05 18:09:31 1997 +0200
+++ b/doc-src/Intro/advanced.tex	Mon May 05 18:50:26 1997 +0200
@@ -368,7 +368,7 @@
 theories, inheriting their types, constants, syntax, etc.  The theory
 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
 \thydx{CPure} offers the more usual higher-order function application
-syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$.
+syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure.
 
 Each theory definition must reside in a separate file, whose name is
 the theory's with {\tt.thy} appended.  Calling
@@ -429,9 +429,9 @@
 the keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are
 rules of the form $s \equiv t$, and should serve only as
 abbreviations. The simplest form of a definition is $f \equiv t$,
-where $f$ is a constant. Also allowed are $\eta$-equivalent forms,
-where the arguments of~$f$ appear applied on the left-hand side of the
-equation instead of abstracted on the right-hand side.
+where $f$ is a constant. Also allowed are $\eta$-equivalent forms of
+this, where the arguments of~$f$ appear applied on the left-hand side
+of the equation instead of abstracted on the right-hand side.
 
 Isabelle checks for common errors in definitions, such as extra
 variables on the right-hand side, but currently does not a complete
diff -r 1a5bfa2ab1d1 -r 5396e99c02af doc-src/Intro/foundations.tex
--- a/doc-src/Intro/foundations.tex	Mon May 05 18:09:31 1997 +0200
+++ b/doc-src/Intro/foundations.tex	Mon May 05 18:50:26 1997 +0200
@@ -1,4 +1,5 @@
 %% $Id$
+
 \part{Foundations} 
 The following sections discuss Isabelle's logical foundations in detail:
 representing logical syntax in the typed $\lambda$-calculus; expressing
@@ -642,8 +643,8 @@
 Resolution expects the rules to have no outer quantifiers~($\Forall$).
 It may rename or instantiate any schematic variables, but leaves free
 variables unchanged.  When constructing a theory, Isabelle puts the
-rules into a standard form containing only schematic variables;
-for instance, $({\imp}E)$ becomes
+rules into a standard form with all free variables converted into
+schematic ones; for instance, $({\imp}E)$ becomes
 \[ \List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}. 
 \]
 When resolving two rules, the unknowns in the first rule are renamed, by