diff -r 2995639c6a09 -r 90695f46440b doc-src/TutorialI/Advanced/advanced.tex --- 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.