# HG changeset patch
# User paulson
# Date 990091744 -7200
# Node ID 9e0708bb15f78bdd62e9d3723c662053ef25d219
# Parent  be41632197036bacc62b9e9c9e15b726ada25bff
minor revisons

diff -r be4163219703 -r 9e0708bb15f7 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed May 16 18:03:12 2001 +0200
+++ b/doc-src/TutorialI/fp.tex	Thu May 17 11:29:04 2001 +0200
@@ -3,9 +3,9 @@
 Although on the surface this chapter is mainly concerned with how to write
 functional programs in HOL and how to verify them, most of the constructs and
 proof procedures introduced are general purpose and recur in any specification
-or verification task. In fact, it we should really speak of functional
-\emph{modelling} rather than \emph{programming} because our aim is not
-primarily to write programs but to design abstract models of systems.  HOL is
+or verification task. In fact, we really should speak of functional
+\emph{modelling} rather than \emph{programming}: our primary aim is not
+to write programs but to design abstract models of systems.  HOL is
 a specification language that goes well beyond what can be expressed as a
 program. However, for the time being we concentrate on the computable.
 
@@ -80,8 +80,8 @@
   \isacommand{redo}\indexbold{*redo}.  Both are only needed at the shell
   level and should not occur in the final theory.
 \item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays
-  the current proof state, for example when it has disappeared off the
-  screen.
+  the current proof state, for example when it has scrolled past the top of
+  the screen.
 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
   print only the first $n$ subgoals from now on and redisplays the current
   proof state. This is helpful when there are many subgoals.