--- a/ProgTutorial/Tactical.thy	Wed Apr 08 09:22:07 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Apr 08 09:55:39 2009 +0200
@@ -1017,8 +1017,9 @@
 
 text {*
   A lot of convenience in the reasoning with Isabelle derives from its
-  powerful simplifier. The power of simplifier is a strength and a weakness at
-  the same time, because you can easily make the simplifier to run into a  loop and its
+  powerful simplifier. The power of the simplifier is a strength and a weakness at
+  the same time, because you can easily make the simplifier run into a loop and
+  in general its
   behaviour can be difficult to predict. There is also a multitude
   of options that you can configure to control the behaviour of the simplifier. 
   We describe some of them in this and the next section.
@@ -1090,7 +1091,7 @@
 
   The rewriting with rules involving preconditions requires what is in
   Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
-  tactics that can be installed in a simpset and which are called during
+  tactics that can be installed in a simpset and which are called at
   various stages during simplification. However, simpsets also include
   simprocs, which can produce rewrite rules on demand (see next
   section). Another component are split-rules, which can simplify for example
@@ -1417,7 +1418,7 @@
 
 text {*
   For all three phases we have to build simpsets adding specific lemmas. As is sufficient
-  for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+  for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
   the desired results. Now we can solve the following lemma
 *}
 
@@ -1483,7 +1484,7 @@
 
 text {*
   where the second argument specifies the pattern and the right-hand side
-  contains the code of the simproc (we have to use @{ML K} since we ignoring
+  contains the code of the simproc (we have to use @{ML K} since we are ignoring
   an argument about morphisms. 
   After this, the simplifier is aware of the simproc and you can test whether 
   it fires on the lemma:
@@ -1638,7 +1639,7 @@
   in choosing the right simpset to which you add a simproc. 
 
   Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
-  with the number @{text n} increase by one. First we implement a function that
+  with the number @{text n} increased by one. First we implement a function that
   takes a term and produces the corresponding integer value.
 *}