--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:46:53 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:55:40 2009 +0100
@@ -523,7 +523,7 @@
   user accidentally. This often broke Isabelle
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
-  usefulness in cases where data needs to be build up dynamically. In the
+  usefulness in cases where data needs to be built up dynamically. In the
   course of this chapter you will learn more about antiquotations:
   they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from the ML-level.
@@ -952,7 +952,7 @@
 
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
-  that can only be build by going through interfaces. As a consequence, every proof 
+  that can only be built by going through interfaces. As a consequence, every proof 
   in Isabelle is correct by construction. This follows the tradition of the LCF approach
   \cite{GordonMilnerWadsworth79}.