--- a/doc-src/TutorialI/Protocol/protocol.tex Tue Dec 18 16:14:56 2001 +0100
+++ b/doc-src/TutorialI/Protocol/protocol.tex Tue Dec 18 16:44:00 2001 +0100
@@ -488,7 +488,9 @@
it is known to the spy. Intuitively, it holds because honest agents
always choose fresh values as nonces; only the spy might reuse a value,
and he doesn't know this particular value. The proof script is short:
-induction, simplification, \isa{blast}.
+induction, simplification, \isa{blast}. The first line uses the rule
+\isa{rev_mp} to prepare the induction by moving two assumptions into the
+induction formula.
\begin{isabelle}
\isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline
\ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\
--- a/doc-src/TutorialI/Rules/rules.tex Tue Dec 18 16:14:56 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Tue Dec 18 16:44:00 2001 +0100
@@ -851,8 +851,8 @@
An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
modified using~\isa{of}, described in
-{\S}\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the
-instantiations may refer to
+{\S}\ref{sec:forward} below. But \isa{rule_tac}, unlike \isa{of}, can
+express instantiations that refer to
\isasymAnd-bound variables in the current subgoal.%
\index{substitution|)}
@@ -1260,8 +1260,9 @@
A definite description is traditionally written $\iota x. P(x)$. It denotes
the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
otherwise, it returns an arbitrary value of the expected type.
-Isabelle uses \sdx{THE} for the Greek letter~$\iota$. (The
-traditional notation could be provided, but it is not legible on screen.)
+Isabelle uses \sdx{THE} for the Greek letter~$\iota$.
+
+%(The traditional notation could be provided, but it is not legible on screen.)
We reason using this rule, where \isa{a} is the unique solution:
\begin{isabelle}
@@ -2301,8 +2302,9 @@
A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one
repetitions of a method. It can also be viewed as the choice between executing a
-method and doing nothing. It is useless at top level but may be valuable within
-other control structures.%
+method and doing nothing. It is useless at top level but can be valuable
+within other control structures; for example,
+\isa{($m$+)?} performs zero or more repetitions of method~$m$.%
\index{tacticals|)}
--- a/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:14:56 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:44:00 2001 +0100
@@ -387,9 +387,8 @@
\cdx{UNION} and \cdx{INTER}\@.
The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.
-We have only scratched the surface of Isabelle/HOL's set theory.
-Hundreds of theorems are proved in theory \isa{Set} and its
-descendants.
+We have only scratched the surface of Isabelle/HOL's set theory, which provides
+hundreds of theorems for your use.
\subsection{Finiteness and Cardinality}
@@ -1070,6 +1069,5 @@
is perhaps the best-known concept defined as a
greatest fixed point. Exhibiting a bisimulation to prove the equality of
two agents in a process algebra is an example of coinduction.
-The coinduction rule can be strengthened in various ways; see
-theory \isa{Gfp} for details.
+The coinduction rule can be strengthened in various ways.
\index{fixed points|)}