doc-src/TutorialI/fp.tex
 changeset 10971 6852682eaf16 parent 10885 90695f46440b child 10978 5eebea8f359f
     1.1 --- a/doc-src/TutorialI/fp.tex	Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/fp.tex	Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -122,11 +122,11 @@
1.4    the files have not been modified).
1.5
1.6    If you suddenly discover that you need to modify a parent theory of your
1.7 -  current theory you must first abandon your current theory\indexbold{abandon
1.8 +  current theory, you must first abandon your current theory\indexbold{abandon
1.9    theory}\indexbold{theory!abandon} (at the shell
1.10    level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
1.11 -  been modified you go back to your original theory. When its first line
1.12 -  \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
1.13 +  been modified, you go back to your original theory. When its first line
1.14 +  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
1.15    modified parent is reloaded automatically.
1.16
1.17    The only time when you need to load a theory by hand is when you simply
1.18 @@ -291,12 +291,12 @@
1.19  \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
1.20  that it did not need to so far. However, when you go beyond toy examples, you
1.21  need to understand the ingredients of \isa{auto}.  This section covers the
1.22 -method that \isa{auto} always applies first, namely simplification.
1.23 +method that \isa{auto} always applies first, simplification.
1.24
1.25  Simplification is one of the central theorem proving tools in Isabelle and
1.26  many other systems. The tool itself is called the \bfindex{simplifier}. The
1.27  purpose of this section is introduce the many features of the simplifier.
1.28 -Anybody intending to use HOL should read this section. Later on
1.29 +Anybody intending to perform proofs in HOL should read this section. Later on
1.30  ({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
1.31  little bit of how the simplifier works. The serious student should read that
1.32  section as well, in particular in order to understand what happened if things
1.33 @@ -359,7 +359,7 @@
1.34  This declaration is a real can of worms.
1.35  In HOL it must be ruled out because it requires a type
1.36  \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
1.37 -same cardinality---an impossibility. For the same reason it is not possible
1.38 +same cardinality --- an impossibility. For the same reason it is not possible
1.39  to allow recursion involving the type \isa{set}, which is isomorphic to
1.40  \isa{t \isasymFun\ bool}.
1.41
1.42 @@ -380,7 +380,7 @@
1.43  \end{isabelle}
1.44  do indeed make sense.  Note the different arrow,