--- a/doc-src/TutorialI/Advanced/advanced.tex Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex Fri Jan 12 16:32:01 2001 +0100
@@ -2,8 +2,7 @@
Although we have already learned a lot about simplification, recursion and
induction, there are some advanced proof techniques that we have not covered
-yet and which are worth knowing about if you intend to beome a serious
-(human) theorem prover. The three sections of this chapter are almost
+yet and which are worth learning. The three sections of this chapter are almost
independent of each other and can be read in any order. Only the notion of
\emph{congruence rules}, introduced in the section on simplification, is
required for parts of the section on recursion.
@@ -19,12 +18,12 @@
and how to deal with partial functions.
If, after reading this section, you feel that the definition of recursive
-functions is overly and maybe unnecessarily complicated by the requirement of
+functions is overly complicated by the requirement of
totality, you should ponder the alternative, a logic of partial functions,
where recursive definitions are always wellformed. For a start, there are many
such logics, and no clear winner has emerged. And in all of these logics you
are (more or less frequently) required to reason about the definedness of
-terms explicitly. Thus one shifts definedness arguments from definition to
+terms explicitly. Thus one shifts definedness arguments from definition time to
proof time. In HOL you may have to work hard to define a function, but proofs
can then proceed unencumbered by worries about undefinedness.