--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:55:40 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 14:20:14 2009 +0100
@@ -1253,7 +1253,7 @@
 text {*
   In the previous section we used \isacommand{setup} in order to make
   a theorem attribute known to Isabelle. What happens behind the scenes
-  is that \isacommand{setup} expects a functions of type 
+  is that \isacommand{setup} expects a function of type 
   @{ML_type "theory -> theory"}: the input theory is the current theory and the 
   output the theory where the theory attribute has been stored.
   
@@ -1309,7 +1309,7 @@
 
   In contrast to an ordinary theory, which simply consists of a type
   signature, as well as tables for constants, axioms and theorems, a local
-  theory also contains additional context information, such as locally fixed
+  theory contains additional context information, such as locally fixed
   variables and local assumptions that may be used by the package. The type
   @{ML_type local_theory} is identical to the type of \emph{proof contexts}
   @{ML_type "Proof.context"}, although not every proof context constitutes a