# HG changeset patch
# User nipkow
# Date 1335251395 -7200
# Node ID c1cca2a052e44a7ccb504b2c42d6df5999b6f9e8
# Parent  4ced561007571af1c3dfe785865fcb4e642cae14
doc update

diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/Bool_nat_list.thy
--- a/doc-src/ProgProve/Thys/Bool_nat_list.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -138,11 +138,11 @@
 Throughout this book, \concept{IH} will stand for ``induction hypothesis''.
 
 We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the
-terse 4 lines explaining the base case and the induction step, and just now a
+terse four lines explaining the base case and the induction step, and just now a
 model of a traditional inductive proof. The three proofs differ in the level
 of detail given and the intended reader: the Isabelle proof is for the
 machine, the informal proofs are for humans. Although this book concentrates
-of Isabelle proofs, it is important to be able to rephrase those proofs
+on Isabelle proofs, it is important to be able to rephrase those proofs
 as informal text comprehensible to a reader familiar with traditional
 mathematical proofs. Later on we will introduce an Isabelle proof language
 that is closer to traditional informal mathematical language and is often
@@ -162,7 +162,7 @@
 
 text{*
 \begin{itemize}
-\item Type @{typ "'a list"} is the type of list over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Type @{typ "'a list"} is the type of lists over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
 \item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}).
 Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
 or @{term"Cons x (Cons y Nil)"} etc.
@@ -218,7 +218,7 @@
 you need to prove
 \begin{enumerate}
 \item the base case @{prop"P(Nil)"} and
-\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text xs}.
+\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
 \end{enumerate}
 This is often called \concept{structural induction}.
 
@@ -302,7 +302,7 @@
 We find that this time @{text"auto"} solves the base case, but the
 induction step merely simplifies to
 @{subgoals[display,indent=0,goals_limit=1]}
-The the missing lemma is associativity of @{const app},
+The missing lemma is associativity of @{const app},
 which we insert in front of the failed lemma @{text rev_app}.
 
 \subsubsection{Associativity of @{const app}}
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/Isar.thy
--- a/doc-src/ProgProve/Thys/Isar.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Isar.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -172,7 +172,7 @@
 \end{tabular}
 \medskip
 
-\noindent The \isacom{using} idiom de-emphasises the used facts by moving them
+\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
 behind the proposition.
 
 \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
@@ -228,7 +228,7 @@
 default. The patterns are phrased in terms of \isacom{show} but work for
 \isacom{have} and \isacom{lemma}, too.
 
-We start with two forms of \concept{case distinction}:
+We start with two forms of \concept{case analysis}:
 starting from a formula @{text P} we have the two cases @{text P} and
 @{prop"~P"}, and starting from a fact @{prop"P \<or> Q"}
 we have the two cases @{text P} and @{text Q}:
@@ -548,7 +548,7 @@
 
 Sometimes one would like to prove some lemma locally within a proof.
 A lemma that shares the current context of assumptions but that
-has its own assumptions and is generalised over its locally fixed
+has its own assumptions and is generalized over its locally fixed
 variables at the end. This is what a \concept{raw proof block} does:
 \begin{quote}
 @{text"{"} \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"}\\
@@ -590,14 +590,14 @@
 the fact just proved, in this case the preceding block. In general,
 \isacom{note} introduces a new name for one or more facts.
 
-\section{Case distinction and induction}
+\section{Case analysis and induction}
 
-\subsection{Datatype case distinction}
+\subsection{Datatype case analysis}
 
-We have seen case distinction on formulas. Now we want to distinguish
+We have seen case analysis on formulas. Now we want to distinguish
 which form some term takes: is it @{text 0} or of the form @{term"Suc n"},
 is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example
-proof by case distinction on the form of @{text xs}:
+proof by case analysis on the form of @{text xs}:
 *}
 
 lemma "length(tl xs) = length xs - 1"
@@ -650,12 +650,12 @@
 Never mind the details, just focus on the pattern:
 *}
 
-lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")
+lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"
 proof (induction n)
   show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp
 next
   fix n assume "\<Sum>{0..n::nat} = n*(n+1) div 2"
-  thus "\<Sum>{0..Suc n::nat} = Suc n*(Suc n+1) div 2" by simp
+  thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp
 qed
 
 text{* Except for the rewrite steps, everything is explicitly given. This
@@ -920,13 +920,13 @@
 
 \subsection{Rule inversion}
 
-Rule inversion is case distinction on which rule could have been used to
+Rule inversion is case analysis of which rule could have been used to
 derive some fact. The name \concept{rule inversion} emphasizes that we are
 reasoning backwards: by which rules could some given fact have been proved?
 For the inductive definition of @{const ev}, rule inversion can be summarized
 like this:
 @{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"}
-The realisation in Isabelle is a case distinction.
+The realisation in Isabelle is a case analysis.
 A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n - 2)"}. We
 already went through the details informally in \autoref{sec:Logic:even}. This
 is the Isar proof:
@@ -946,7 +946,7 @@
 end
 (*>*)
 
-text{* The key point here is that a case distinction over some inductively
+text{* The key point here is that a case analysis over some inductively
 defined predicate is triggered by piping the given fact
 (here: \isacom{from}~@{text this}) into a proof by @{text cases}.
 Let us examine the assumptions available in each case. In case @{text ev0}
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/Logic.thy
--- a/doc-src/ProgProve/Thys/Logic.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Logic.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -5,12 +5,12 @@
 (*>*)
 text{*
 \vspace{-5ex}
-\section{Logic and Proof Beyond Equality}
+\section{Logic and proof beyond equality}
 \label{sec:Logic}
 
 \subsection{Formulas}
 
-The basic syntax of formulas (\textit{form} below)
+The core syntax of formulas (\textit{form} below)
 provides the standard logical constructs, in decreasing precedence:
 \[
 \begin{array}{rcl}
@@ -27,14 +27,14 @@
  &\mid& @{prop"\<forall>x. form"} ~\mid~  @{prop"\<exists>x. form"}
 \end{array}
 \]
-Terms are the ones we have seen all along, built from constant, variables,
+Terms are the ones we have seen all along, built from constants, variables,
 function application and @{text"\<lambda>"}-abstraction, including all the syntactic
 sugar like infix symbols, @{text "if"}, @{text "case"} etc.
 \begin{warn}
 Remember that formulas are simply terms of type @{text bool}. Hence
 @{text "="} also works for formulas. Beware that @{text"="} has a higher
 precedence than the other logical operators. Hence @{prop"s = t \<and> A"} means
-@{text"(s = t) \<and> A"}, and @{prop"A\<and>B = B\<and>A"} means @{text"A \<and> (B = A) \<and> B"}.
+@{text"(s = t) \<and> A"}, and @{prop"A\<and>B = B\<and>A"} means @{text"A \<and> (B = B) \<and> A"}.
 Logical equivalence can also be written with
 @{text "\<longleftrightarrow>"} instead of @{text"="}, where @{text"\<longleftrightarrow>"} has the same low
 precedence as @{text"\<longrightarrow>"}. Hence @{text"A \<and> B \<longleftrightarrow> B \<and> A"} really means
@@ -51,7 +51,7 @@
 @{text "\<exists>"} & \xsymbol{exists} & \texttt{EX}\\
 @{text "\<lambda>"} & \xsymbol{lambda} & \texttt{\%}\\
 @{text "\<longrightarrow>"} & \texttt{-{}->}\\
-@{text "\<longleftrightarrow>"} & \texttt{<-{}->}\\
+@{text "\<longleftrightarrow>"} & \texttt{<->}\\
 @{text "\<and>"} & \texttt{/\char`\\} & \texttt{\&}\\
 @{text "\<or>"} & \texttt{\char`\\/} & \texttt{|}\\
 @{text "\<not>"} & \xsymbol{not} & \texttt{\char`~}\\
@@ -63,7 +63,7 @@
 and the third column shows ASCII representations that stay fixed.
 \begin{warn}
 The implication @{text"\<Longrightarrow>"} is part of the Isabelle framework. It structures
-theorems and proof states, separating assumptions from conclusion.
+theorems and proof states, separating assumptions from conclusions.
 The implication @{text"\<longrightarrow>"} is part of the logic HOL and can occur inside the
 formulas that make up the assumptions and conclusion.
 Theorems should be of the form @{text"\<lbrakk> A\<^isub>1; \<dots>; A\<^isub>n \<rbrakk> \<Longrightarrow> A"},
@@ -74,7 +74,7 @@
 \subsection{Sets}
 
 Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
-They can be finite or infinite. Sets come with the usual notations:
+They can be finite or infinite. Sets come with the usual notation:
 \begin{itemize}
 \item @{term"{}"},\quad @{text"{e\<^isub>1,\<dots>,e\<^isub>n}"}
 \item @{prop"e \<in> A"},\quad @{prop"A \<subseteq> B"}
@@ -87,7 +87,7 @@
 \begin{warn}
 In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
 involving a proper term @{text t} must be written
-@{term[source]"{t |x y z. P}"},
+@{term[source]"{t | x y z. P}"},
 where @{text "x y z"} are the free variables in @{text t}.
 This is just a shorthand for @{term"{v. EX x y z. v = t \<and> P}"}, where
 @{text v} is a new variable.
@@ -153,8 +153,8 @@
 succeeds where @{text fastforce} fails.
 
 The method of choice for complex logical goals is @{text blast}. In the
-following example, @{text T} and @{text A} are two binary predicates, and it
-is shown that @{text T} is total, @{text A} is antisymmetric and @{text T} is
+following example, @{text T} and @{text A} are two binary predicates. It
+is shown that if @{text T} is total, @{text A} is antisymmetric and @{text T} is
 a subset of @{text A}, then @{text A} is a subset of @{text T}:
 *}
 
@@ -344,12 +344,12 @@
 automatically selects the appropriate rule for the current subgoal.
 
 You can also turn your own theorems into introduction rules by giving them
-them @{text"intro"} attribute, analogous to the @{text simp} attribute.  In
+the @{text"intro"} attribute, analogous to the @{text simp} attribute.  In
 that case @{text blast}, @{text fastforce} and (to a limited extent) @{text
 auto} will automatically backchain with those theorems. The @{text intro}
 attribute should be used with care because it increases the search space and
-can lead to nontermination.  Sometimes it is better to use it only in a
-particular calls of @{text blast} and friends. For example,
+can lead to nontermination.  Sometimes it is better to use it only in
+specific calls of @{text blast} and friends. For example,
 @{thm[source] le_trans}, transitivity of @{text"\<le>"} on type @{typ nat},
 is not an introduction rule by default because of the disastrous effect
 on the search space, but can be useful in specific situations:
@@ -419,8 +419,11 @@
 \label{sec:inductive-defs}
 
 Inductive definitions are the third important definition facility, after
-datatypes and recursive function. In fact, they are the key construct in the
+datatypes and recursive function.
+\sem
+In fact, they are the key construct in the
 definition of operational semantics in the second part of the book.
+\endsem
 
 \subsection{An example: even numbers}
 \label{sec:Logic:even}
@@ -506,9 +509,9 @@
 case @{thm[source]evSS} we have \mbox{@{prop"m = n+(2::nat)"}} and may assume
 @{prop"ev n"}, which implies @{prop"ev (m - 2)"} because @{text"m - 2 = (n +
 2) - 2 = n"}. We did not need the induction hypothesis at all for this proof,
-it is just a case distinction on which rule was used, but having @{prop"ev
+it is just a case analysis of which rule was used, but having @{prop"ev
 n"} at our disposal in case @{thm[source]evSS} was essential.
-This case distinction over rules is also called ``rule inversion''
+This case analysis of rules is also called ``rule inversion''
 and is discussed in more detail in \autoref{ch:Isar}.
 
 \subsubsection{In Isabelle}
@@ -589,7 +592,7 @@
 definition only expresses the positive information directly. The negative
 information, for example, that @{text 1} is not even, has to be proved from
 it (by induction or rule inversion). On the other hand, rule induction is
-Taylor made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you
+tailor-made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you
 to prove the positive cases. In the proof of @{prop"even n \<Longrightarrow> P n"} by
 computation induction via @{thm[source]even.induct}, we are also presented
 with the trivial negative cases. If you want the convenience of both
@@ -599,8 +602,8 @@
 
 But many concepts do not admit a recursive definition at all because there is
 no datatype for the recursion (for example, the transitive closure of a
-relation), or the recursion would not terminate (for example, the operational
-semantics in the second part of this book). Even if there is a recursive
+relation), or the recursion would not terminate (for example,
+an interpreter for a programming language). Even if there is a recursive
 definition, if we are only interested in the positive information, the
 inductive definition may be much simpler.
 
@@ -609,8 +612,11 @@
 
 Evenness is really more conveniently expressed recursively than inductively.
 As a second and very typical example of an inductive definition we define the
-reflexive transitive closure. It will also be an important building block for
+reflexive transitive closure.
+\sem
+It will also be an important building block for
 some of the semantics considered in the second part of the book.
+\endsem
 
 The reflexive transitive closure, called @{text star} below, is a function
 that maps a binary predicate to another binary predicate: if @{text r} is of
@@ -628,8 +634,8 @@
 
 text{* The base case @{thm[source] refl} is reflexivity: @{term "x=y"}. The
 step case @{thm[source]step} combines an @{text r} step (from @{text x} to
-@{text y}) and a @{const star} step (from @{text y} to @{text z}) into a
-@{const star} step (from @{text x} to @{text z}).
+@{text y}) and a @{term"star r"} step (from @{text y} to @{text z}) into a
+@{term"star r"} step (from @{text x} to @{text z}).
 The ``\isacom{for}~@{text r}'' in the header is merely a hint to Isabelle
 that @{text r} is a fixed parameter of @{const star}, in contrast to the
 further parameters of @{const star}, which change. As a result, Isabelle
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/Types_and_funs.thy
--- a/doc-src/ProgProve/Thys/Types_and_funs.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Types_and_funs.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -132,12 +132,12 @@
 function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by
 subtracting @{term"f n"} on both sides.
 
-Isabelle automatic termination checker requires that the arguments of
+Isabelle's automatic termination checker requires that the arguments of
 recursive calls on the right-hand side must be strictly smaller than the
 arguments on the left-hand side. In the simplest case, this means that one
 fixed argument position decreases in size with each recursive call. The size
 is measured as the number of constructors (excluding 0-ary ones, e.g.\ @{text
-Nil}). Lexicographic combinations are also recognised. In more complicated
+Nil}). Lexicographic combinations are also recognized. In more complicated
 situations, the user may have to prove termination by hand. For details
 see~\cite{Krauss}.
 
@@ -152,7 +152,7 @@
 "div2 (Suc(Suc n)) = Suc(div2 n)"
 
 text{* does not just define @{const div2} but also proves a
-customised induction rule:
+customized induction rule:
 \[
 \inferrule{
 \mbox{@{thm (prem 1) div2.induct}}\\
@@ -160,7 +160,7 @@
 \mbox{@{thm (prem 3) div2.induct}}}
 {\mbox{@{thm (concl) div2.induct[of _ "m"]}}}
 \]
-This customised induction rule can simplify inductive proofs. For example,
+This customized induction rule can simplify inductive proofs. For example,
 *}
 
 lemma "div2(n+n) = n"
@@ -171,7 +171,7 @@
 An application of @{text auto} finishes the proof.
 Had we used ordinary structural induction on @{text n},
 the proof would have needed an additional
-case distinction in the induction step.
+case analysis in the induction step.
 
 The general case is often called \concept{computation induction},
 because the induction follows the (terminating!) computation.
@@ -202,7 +202,7 @@
  if the function is defined by recursion on argument number $i$.}
 \end{quote}
 The key heuristic, and the main point of this section, is to
-\emph{generalise the goal before induction}.
+\emph{generalize the goal before induction}.
 The reason is simple: if the goal is
 too specific, the induction hypothesis is too weak to allow the induction
 step to go through. Let us illustrate the idea with an example.
@@ -218,12 +218,12 @@
 done
 (*>*)
 fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"itrev []     ys = ys" |
+"itrev []        ys = ys" |
 "itrev (x#xs) ys = itrev xs (x#ys)"
 
 text{* The behaviour of @{const itrev} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
-and returning that second argument when the first one becomes
+and it returns that second argument when the first one becomes
 empty. Note that @{const itrev} is tail-recursive: it can be
 compiled into a loop, no stack is necessary for executing it.
 
@@ -247,10 +247,10 @@
 argument,~@{term"[]"}, prevents it from rewriting the conclusion.  
 This example suggests a heuristic:
 \begin{quote}
-\emph{Generalise goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
 Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is
-just not true.  The correct generalisation is
+just not true.  The correct generalization is
 *};
 (*<*)oops;(*>*)
 lemma "itrev xs ys = rev xs @ ys"
@@ -258,7 +258,7 @@
 txt{*
 If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to
 @{term"rev xs"}, as required.
-In this instance it was easy to guess the right generalisation.
+In this instance it was easy to guess the right generalization.
 Other situations can require a good deal of creativity.  
 
 Although we now have two variables, only @{text xs} is suitable for
@@ -266,12 +266,12 @@
 not there:
 @{subgoals[display,margin=65]}
 The induction hypothesis is still too weak, but this time it takes no
-intuition to generalise: the problem is that the @{text ys}
+intuition to generalize: the problem is that the @{text ys}
 in the induction hypothesis is fixed,
 but the induction hypothesis needs to be applied with
 @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
 for all @{text ys} instead of a fixed one. We can instruct induction
-to perform this generalisation for us by adding @{text "arbitrary: ys"}.
+to perform this generalization for us by adding @{text "arbitrary: ys"}.
 *}
 (*<*)oops
 lemma "itrev xs ys = rev xs @ ys"
@@ -287,12 +287,12 @@
 done
 
 text{*
-This leads to another heuristic for generalisation:
+This leads to another heuristic for generalization:
 \begin{quote}
-\emph{Generalise induction by generalising all free
+\emph{Generalize induction by generalizing all free
 variables\\ {\em(except the induction variable itself)}.}
 \end{quote}
-Generalisation is best performed with @{text"arbitrary: y\<^isub>1 \<dots> y\<^isub>k"}. 
+Generalization is best performed with @{text"arbitrary: y\<^isub>1 \<dots> y\<^isub>k"}. 
 This heuristic prevents trivial failures like the one above.
 However, it should not be applied blindly.
 It is not always required, and the additional quantifiers can complicate
@@ -306,7 +306,7 @@
 \item using equations $l = r$ from left to right (only),
 \item as long as possible.
 \end{itemize}
-To emphasise the directionality, equations that have been given the
+To emphasize the directionality, equations that have been given the
 @{text"simp"} attribute are called \concept{simplification}
 rules. Logically, they are still symmetric, but proofs by
 simplification use them only in the left-to-right direction.  The proof tool
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/document/Bool_nat_list.tex
--- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -192,11 +192,11 @@
 Throughout this book, \concept{IH} will stand for ``induction hypothesis''.
 
 We have now seen three proofs of \isa{add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}: the Isabelle one, the
-terse 4 lines explaining the base case and the induction step, and just now a
+terse four lines explaining the base case and the induction step, and just now a
 model of a traditional inductive proof. The three proofs differ in the level
 of detail given and the intended reader: the Isabelle proof is for the
 machine, the informal proofs are for humans. Although this book concentrates
-of Isabelle proofs, it is important to be able to rephrase those proofs
+on Isabelle proofs, it is important to be able to rephrase those proofs
 as informal text comprehensible to a reader familiar with traditional
 mathematical proofs. Later on we will introduce an Isabelle proof language
 that is closer to traditional informal mathematical language and is often
@@ -219,7 +219,7 @@
 \ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \begin{itemize}
-\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of list over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of lists over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
 \item Lists have two constructors: \isa{Nil}, the empty list, and \isa{Cons}, which puts an element (of type \isa{{\isaliteral{27}{\isacharprime}}a}) in front of a list (of type \isa{{\isaliteral{27}{\isacharprime}}a\ list}).
 Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil},
 or \isa{Cons\ x\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ Nil{\isaliteral{29}{\isacharparenright}}} etc.
@@ -282,7 +282,7 @@
 you need to prove
 \begin{enumerate}
 \item the base case \isa{P\ Nil} and
-\item the inductive case \isa{P\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}} under the assumption \isa{P\ xs}, for some arbitrary but fixed \isa{xs}.
+\item the inductive case \isa{P\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}} under the assumption \isa{P\ xs}, for some arbitrary but fixed \isa{x} and \isa{xs}.
 \end{enumerate}
 This is often called \concept{structural induction}.
 
@@ -435,7 +435,7 @@
 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
-The the missing lemma is associativity of \isa{app},
+The missing lemma is associativity of \isa{app},
 which we insert in front of the failed lemma \isa{rev{\isaliteral{5F}{\isacharunderscore}}app}.
 
 \subsubsection{Associativity of \isa{app}}
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/document/Isar.tex
--- a/doc-src/ProgProve/Thys/document/Isar.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Isar.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -263,7 +263,7 @@
 \end{tabular}
 \medskip
 
-\noindent The \isacom{using} idiom de-emphasises the used facts by moving them
+\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
 behind the proposition.
 
 \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
@@ -339,7 +339,7 @@
 default. The patterns are phrased in terms of \isacom{show} but work for
 \isacom{have} and \isacom{lemma}, too.
 
-We start with two forms of \concept{case distinction}:
+We start with two forms of \concept{case analysis}:
 starting from a formula \isa{P} we have the two cases \isa{P} and
 \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, and starting from a fact \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}
 we have the two cases \isa{P} and \isa{Q}:%
@@ -946,7 +946,7 @@
 
 Sometimes one would like to prove some lemma locally within a proof.
 A lemma that shares the current context of assumptions but that
-has its own assumptions and is generalised over its locally fixed
+has its own assumptions and is generalized over its locally fixed
 variables at the end. This is what a \concept{raw proof block} does:
 \begin{quote}
 \isa{{\isaliteral{7B}{\isacharbraceleft}}} \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}\\
@@ -1016,14 +1016,14 @@
 the fact just proved, in this case the preceding block. In general,
 \isacom{note} introduces a new name for one or more facts.
 
-\section{Case distinction and induction}
+\section{Case analysis and induction}
 
-\subsection{Datatype case distinction}
+\subsection{Datatype case analysis}
 
-We have seen case distinction on formulas. Now we want to distinguish
+We have seen case analysis on formulas. Now we want to distinguish
 which form some term takes: is it \isa{{\isadigit{0}}} or of the form \isa{Suc\ n},
 is it \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} or of the form \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, etc. Here is a typical example
-proof by case distinction on the form of \isa{xs}:%
+proof by case analysis on the form of \isa{xs}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
@@ -1123,7 +1123,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 %
@@ -1141,7 +1141,7 @@
 \ n\ \isacommand{assume}\isamarkupfalse%
 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
@@ -1548,7 +1548,7 @@
 
 \subsection{Rule inversion}
 
-Rule inversion is case distinction on which rule could have been used to
+Rule inversion is case analysis of which rule could have been used to
 derive some fact. The name \concept{rule inversion} emphasizes that we are
 reasoning backwards: by which rules could some given fact have been proved?
 For the inductive definition of \isa{ev}, rule inversion can be summarized
@@ -1556,7 +1556,7 @@
 \begin{isabelle}%
 ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ev\ k{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
-The realisation in Isabelle is a case distinction.
+The realisation in Isabelle is a case analysis.
 A simple example is the proof that \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. We
 already went through the details informally in \autoref{sec:Logic:even}. This
 is the Isar proof:%
@@ -1595,7 +1595,7 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-The key point here is that a case distinction over some inductively
+The key point here is that a case analysis over some inductively
 defined predicate is triggered by piping the given fact
 (here: \isacom{from}~\isa{this}) into a proof by \isa{cases}.
 Let us examine the assumptions available in each case. In case \isa{ev{\isadigit{0}}}
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/document/Logic.tex
--- a/doc-src/ProgProve/Thys/document/Logic.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -17,12 +17,12 @@
 %
 \begin{isamarkuptext}%
 \vspace{-5ex}
-\section{Logic and Proof Beyond Equality}
+\section{Logic and proof beyond equality}
 \label{sec:Logic}
 
 \subsection{Formulas}
 
-The basic syntax of formulas (\textit{form} below)
+The core syntax of formulas (\textit{form} below)
 provides the standard logical constructs, in decreasing precedence:
 \[
 \begin{array}{rcl}
@@ -39,14 +39,14 @@
  &\mid& \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ form} ~\mid~  \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ form}
 \end{array}
 \]
-Terms are the ones we have seen all along, built from constant, variables,
+Terms are the ones we have seen all along, built from constants, variables,
 function application and \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstraction, including all the syntactic
 sugar like infix symbols, \isa{if}, \isa{case} etc.
 \begin{warn}
 Remember that formulas are simply terms of type \isa{bool}. Hence
 \isa{{\isaliteral{3D}{\isacharequal}}} also works for formulas. Beware that \isa{{\isaliteral{3D}{\isacharequal}}} has a higher
 precedence than the other logical operators. Hence \isa{s\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means
-\isa{{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}, and \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}.
+\isa{{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}, and \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}.
 Logical equivalence can also be written with
 \isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} instead of \isa{{\isaliteral{3D}{\isacharequal}}}, where \isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} has the same low
 precedence as \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. Hence \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} really means
@@ -63,7 +63,7 @@
 \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} & \xsymbol{exists} & \texttt{EX}\\
 \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} & \xsymbol{lambda} & \texttt{\%}\\
 \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} & \texttt{-{}->}\\
-\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} & \texttt{<-{}->}\\
+\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} & \texttt{<->}\\
 \isa{{\isaliteral{5C3C616E643E}{\isasymand}}} & \texttt{/\char`\\} & \texttt{\&}\\
 \isa{{\isaliteral{5C3C6F723E}{\isasymor}}} & \texttt{\char`\\/} & \texttt{|}\\
 \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}} & \xsymbol{not} & \texttt{\char`~}\\
@@ -75,7 +75,7 @@
 and the third column shows ASCII representations that stay fixed.
 \begin{warn}
 The implication \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} is part of the Isabelle framework. It structures
-theorems and proof states, separating assumptions from conclusion.
+theorems and proof states, separating assumptions from conclusions.
 The implication \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} is part of the logic HOL and can occur inside the
 formulas that make up the assumptions and conclusion.
 Theorems should be of the form \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A},
@@ -86,7 +86,7 @@
 \subsection{Sets}
 
 Sets of elements of type \isa{{\isaliteral{27}{\isacharprime}}a} have type \isa{{\isaliteral{27}{\isacharprime}}a\ set}.
-They can be finite or infinite. Sets come with the usual notations:
+They can be finite or infinite. Sets come with the usual notation:
 \begin{itemize}
 \item \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}},\quad \isa{{\isaliteral{7B}{\isacharbraceleft}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}}
 \item \isa{e\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A},\quad \isa{A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B}
@@ -99,7 +99,7 @@
 \begin{warn}
 In \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}} the \isa{x} must be a variable. Set comprehension
 involving a proper term \isa{t} must be written
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}t\ {\isaliteral{7C}{\isacharbar}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
+\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}t\ {\isaliteral{7C}{\isacharbar}}\ x\ y\ z{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
 where \isa{x\ y\ z} are the free variables in \isa{t}.
 This is just a shorthand for \isa{{\isaliteral{7B}{\isacharbraceleft}}v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ v\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P{\isaliteral{7D}{\isacharbraceright}}}, where
 \isa{v} is a new variable.
@@ -210,8 +210,8 @@
 succeeds where \isa{fastforce} fails.
 
 The method of choice for complex logical goals is \isa{blast}. In the
-following example, \isa{T} and \isa{A} are two binary predicates, and it
-is shown that \isa{T} is total, \isa{A} is antisymmetric and \isa{T} is
+following example, \isa{T} and \isa{A} are two binary predicates. It
+is shown that if \isa{T} is total, \isa{A} is antisymmetric and \isa{T} is
 a subset of \isa{A}, then \isa{A} is a subset of \isa{T}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -449,11 +449,11 @@
 automatically selects the appropriate rule for the current subgoal.
 
 You can also turn your own theorems into introduction rules by giving them
-them \isa{intro} attribute, analogous to the \isa{simp} attribute.  In
+the \isa{intro} attribute, analogous to the \isa{simp} attribute.  In
 that case \isa{blast}, \isa{fastforce} and (to a limited extent) \isa{auto} will automatically backchain with those theorems. The \isa{intro}
 attribute should be used with care because it increases the search space and
-can lead to nontermination.  Sometimes it is better to use it only in a
-particular calls of \isa{blast} and friends. For example,
+can lead to nontermination.  Sometimes it is better to use it only in
+specific calls of \isa{blast} and friends. For example,
 \isa{le{\isaliteral{5F}{\isacharunderscore}}trans}, transitivity of \isa{{\isaliteral{5C3C6C653E}{\isasymle}}} on type \isa{nat},
 is not an introduction rule by default because of the disastrous effect
 on the search space, but can be useful in specific situations:%
@@ -550,8 +550,11 @@
 \label{sec:inductive-defs}
 
 Inductive definitions are the third important definition facility, after
-datatypes and recursive function. In fact, they are the key construct in the
+datatypes and recursive function.
+\sem
+In fact, they are the key construct in the
 definition of operational semantics in the second part of the book.
+\endsem
 
 \subsection{An example: even numbers}
 \label{sec:Logic:even}
@@ -639,8 +642,8 @@
 from \isa{ev\ {\isadigit{0}}} because \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} on type \isa{nat}. In
 case \isa{evSS} we have \mbox{\isa{m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}}} and may assume
 \isa{ev\ n}, which implies \isa{ev\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} because \isa{m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n}. We did not need the induction hypothesis at all for this proof,
-it is just a case distinction on which rule was used, but having \isa{ev\ n} at our disposal in case \isa{evSS} was essential.
-This case distinction over rules is also called ``rule inversion''
+it is just a case analysis of which rule was used, but having \isa{ev\ n} at our disposal in case \isa{evSS} was essential.
+This case analysis of rules is also called ``rule inversion''
 and is discussed in more detail in \autoref{ch:Isar}.
 
 \subsubsection{In Isabelle}
@@ -789,7 +792,7 @@
 definition only expresses the positive information directly. The negative
 information, for example, that \isa{{\isadigit{1}}} is not even, has to be proved from
 it (by induction or rule inversion). On the other hand, rule induction is
-Taylor made for proving \mbox{\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}} because it only asks you
+tailor-made for proving \mbox{\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}} because it only asks you
 to prove the positive cases. In the proof of \isa{even\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n} by
 computation induction via \isa{even{\isaliteral{2E}{\isachardot}}induct}, we are also presented
 with the trivial negative cases. If you want the convenience of both
@@ -799,8 +802,8 @@
 
 But many concepts do not admit a recursive definition at all because there is
 no datatype for the recursion (for example, the transitive closure of a
-relation), or the recursion would not terminate (for example, the operational
-semantics in the second part of this book). Even if there is a recursive
+relation), or the recursion would not terminate (for example,
+an interpreter for a programming language). Even if there is a recursive
 definition, if we are only interested in the positive information, the
 inductive definition may be much simpler.
 
@@ -809,8 +812,11 @@
 
 Evenness is really more conveniently expressed recursively than inductively.
 As a second and very typical example of an inductive definition we define the
-reflexive transitive closure. It will also be an important building block for
+reflexive transitive closure.
+\sem
+It will also be an important building block for
 some of the semantics considered in the second part of the book.
+\endsem
 
 The reflexive transitive closure, called \isa{star} below, is a function
 that maps a binary predicate to another binary predicate: if \isa{r} is of
@@ -828,8 +834,8 @@
 \begin{isamarkuptext}%
 The base case \isa{refl} is reflexivity: \isa{x\ {\isaliteral{3D}{\isacharequal}}\ y}. The
 step case \isa{step} combines an \isa{r} step (from \isa{x} to
-\isa{y}) and a \isa{star} step (from \isa{y} to \isa{z}) into a
-\isa{star} step (from \isa{x} to \isa{z}).
+\isa{y}) and a \isa{star\ r} step (from \isa{y} to \isa{z}) into a
+\isa{star\ r} step (from \isa{x} to \isa{z}).
 The ``\isacom{for}~\isa{r}'' in the header is merely a hint to Isabelle
 that \isa{r} is a fixed parameter of \isa{star}, in contrast to the
 further parameters of \isa{star}, which change. As a result, Isabelle
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/document/Types_and_funs.tex
--- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -169,11 +169,11 @@
 function \isa{f\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} and conclude \mbox{\isa{{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}}} by
 subtracting \isa{f\ n} on both sides.
 
-Isabelle automatic termination checker requires that the arguments of
+Isabelle's automatic termination checker requires that the arguments of
 recursive calls on the right-hand side must be strictly smaller than the
 arguments on the left-hand side. In the simplest case, this means that one
 fixed argument position decreases in size with each recursive call. The size
-is measured as the number of constructors (excluding 0-ary ones, e.g.\ \isa{Nil}). Lexicographic combinations are also recognised. In more complicated
+is measured as the number of constructors (excluding 0-ary ones, e.g.\ \isa{Nil}). Lexicographic combinations are also recognized. In more complicated
 situations, the user may have to prove termination by hand. For details
 see~\cite{Krauss}.
 
@@ -189,7 +189,7 @@
 {\isaliteral{22}{\isachardoublequoteopen}}div{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc{\isaliteral{28}{\isacharparenleft}}div{\isadigit{2}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 does not just define \isa{div{\isadigit{2}}} but also proves a
-customised induction rule:
+customized induction rule:
 \[
 \inferrule{
 \mbox{\isa{P\ {\isadigit{0}}}}\\
@@ -197,7 +197,7 @@
 \mbox{\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ P\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}}}
 {\mbox{\isa{P\ m}}}
 \]
-This customised induction rule can simplify inductive proofs. For example,%
+This customized induction rule can simplify inductive proofs. For example,%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
@@ -221,7 +221,7 @@
 An application of \isa{auto} finishes the proof.
 Had we used ordinary structural induction on \isa{n},
 the proof would have needed an additional
-case distinction in the induction step.
+case analysis in the induction step.
 
 The general case is often called \concept{computation induction},
 because the induction follows the (terminating!) computation.
@@ -252,7 +252,7 @@
  if the function is defined by recursion on argument number $i$.}
 \end{quote}
 The key heuristic, and the main point of this section, is to
-\emph{generalise the goal before induction}.
+\emph{generalize the goal before induction}.
 The reason is simple: if the goal is
 too specific, the induction hypothesis is too weak to allow the induction
 step to go through. Let us illustrate the idea with an example.
@@ -273,12 +273,12 @@
 \endisadelimproof
 \isacommand{fun}\isamarkupfalse%
 \ itrev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
 {\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 The behaviour of \isa{itrev} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
-and returning that second argument when the first one becomes
+and it returns that second argument when the first one becomes
 empty. Note that \isa{itrev} is tail-recursive: it can be
 compiled into a loop, no stack is necessary for executing it.
 
@@ -312,10 +312,10 @@
 argument,~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, prevents it from rewriting the conclusion.  
 This example suggests a heuristic:
 \begin{quote}
-\emph{Generalise goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
 Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs} is
-just not true.  The correct generalisation is%
+just not true.  The correct generalization is%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 %
@@ -336,7 +336,7 @@
 \begin{isamarkuptxt}%
 If \isa{ys} is replaced by \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, the right-hand side simplifies to
 \isa{rev\ xs}, as required.
-In this instance it was easy to guess the right generalisation.
+In this instance it was easy to guess the right generalization.
 Other situations can require a good deal of creativity.  
 
 Although we now have two variables, only \isa{xs} is suitable for
@@ -348,12 +348,12 @@
 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ ys%
 \end{isabelle}
 The induction hypothesis is still too weak, but this time it takes no
-intuition to generalise: the problem is that the \isa{ys}
+intuition to generalize: the problem is that the \isa{ys}
 in the induction hypothesis is fixed,
 but the induction hypothesis needs to be applied with
 \isa{a\ {\isaliteral{23}{\isacharhash}}\ ys} instead of \isa{ys}. Hence we prove the theorem
 for all \isa{ys} instead of a fixed one. We can instruct induction
-to perform this generalisation for us by adding \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ ys}.%
+to perform this generalization for us by adding \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ ys}.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 %
@@ -394,12 +394,12 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-This leads to another heuristic for generalisation:
+This leads to another heuristic for generalization:
 \begin{quote}
-\emph{Generalise induction by generalising all free
+\emph{Generalize induction by generalizing all free
 variables\\ {\em(except the induction variable itself)}.}
 \end{quote}
-Generalisation is best performed with \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub k}. 
+Generalization is best performed with \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub k}. 
 This heuristic prevents trivial failures like the one above.
 However, it should not be applied blindly.
 It is not always required, and the additional quantifiers can complicate
@@ -413,7 +413,7 @@
 \item using equations $l = r$ from left to right (only),
 \item as long as possible.
 \end{itemize}
-To emphasise the directionality, equations that have been given the
+To emphasize the directionality, equations that have been given the
 \isa{simp} attribute are called \concept{simplification}
 rules. Logically, they are still symmetric, but proofs by
 simplification use them only in the left-to-right direction.  The proof tool