doc-src/TutorialI/Advanced/Partial.thy

 (*<*)theory Partial = While_Combinator:(*>*)
 
 text{*\noindent Throughout the tutorial we have emphasized the fact
 that all functions in HOL are total. Hence we cannot hope to define
-truly partial functions but must totalize them. A straightforward
-totalization is to lift the result type of the function from $\tau$ to
+truly partial functions, but must make them total.  A straightforward
+method is to lift the result type of the function from $\tau$ to
 $\tau$~@{text option} (see \ref{sec:option}), where @{term None} is
 returned if the function is applied to an argument not in its
 domain. Function @{term assoc} in \S\ref{sec:Trie} is a simple example.
 We do not pursue this schema further because it should be clear
 how it works. Its main drawback is that the result of such a lifted

    fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"
 
 text{*\noindent
 The loop operates on two ``local variables'' @{term x} and @{term x'}
 containing the ``current'' and the ``next'' value of function @{term f}.
-They are initalized with the global @{term x} and @{term"f x"}. At the
+They are initialized with the global @{term x} and @{term"f x"}. At the
 end @{term fst} selects the local @{term x}.
 
 Although the definition of tail recursive functions via @{term while} avoids
 termination proofs, there is no free lunch. When proving properties of
 functions defined by @{term while}, termination rears its ugly head

 done
 
 text{* Let us conclude this section on partial functions by a
 discussion of the merits of the @{term while} combinator. We have
 already seen that the advantage (if it is one) of not having to
-provide a termintion argument when defining a function via @{term
+provide a termination argument when defining a function via @{term
 while} merely puts off the evil hour. On top of that, tail recursive
 functions tend to be more complicated to reason about. So why use
 @{term while} at all? The only reason is executability: the recursion
 equation for @{term while} is a directly executable functional
 program. This is in stark contrast to guarded recursion as introduced