--- a/ProgTutorial/Tactical.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -18,13 +18,13 @@
   Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996.
   \end{flushright}
 
-  One of the main reason for descending to the ML-level of Isabelle is to be
-  able to implement automatic proof procedures. Such proof procedures can
+  One of the main reason for descending to the ML-level of Isabelle is to
+  implement automatic proof procedures. Such proof procedures can
   considerably lessen the burden of manual reasoning. They are centred around
   the idea of refining a goal state using tactics. This is similar to the
   \isacommand{apply}-style reasoning at the user-level, where goals are
   modified in a sequence of proof steps until all of them are discharged.
-  In this chapter we will explain simple tactics and how to combine them using
+  In this chapter we explain how to implement simple tactics and how to combine them using
   tactic combinators. We also describe the simplifier, simprocs and conversions.
 *}
 
@@ -113,7 +113,7 @@
 text {*
   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
   user-level of Isabelle the tactic @{ML foo_tac} or 
-  any other function that returns a tactic. There are some goal transformation
+  any other function that returns a tactic. There are some goal transformations
   that are performed by @{text "tactic"}. They can be avoided by using 
   @{text "raw_tactic"} instead.
 
@@ -138,7 +138,7 @@
   one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you
   can give the number for the subgoal explicitly when the tactic is called. So
   in the next proof you can first discharge the second subgoal, and
-  subsequently the first.
+  then the first.
 *}
 
 lemma 
@@ -152,8 +152,8 @@
   This kind of addressing is more difficult to achieve when the goal is 
   hard-coded inside the tactic. 
 
-  The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing
-  goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
+  The tactics @{ML foo_tac} and @{ML foo_tac'} are specific
+  to goals of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
   this form, then these tactics return the error message:\footnote{To be
   precise, tactics do not produce this error message; the message originates from the
   \isacommand{apply} wrapper that calls the tactic.}
@@ -173,8 +173,8 @@
 
 text {*
   By convention, if a tactic fails, then it should return the empty sequence. 
-  Therefore, if you write your own tactics, they  should not raise exceptions 
-  willy-nilly; only in very grave failure situations should a tactic raise the 
+  Therefore, your own tactics should not raise exceptions 
+  willy-nilly; only in very grave failure situations should a tactic raise the
   exception @{text THM}.
 
   The simplest tactics are @{ML_ind no_tac in Tactical} and