# HG changeset patch
# User griff
# Date 1237812940 -3600
# Node ID e1dbcccf970fbeb3cb62144edcbb58f58529175d
# Parent  f9b7bf8aad3e62f43c377fe312056bc7db2e865d
passive of `build' = `built'

diff -r f9b7bf8aad3e -r e1dbcccf970f ProgTutorial/FirstSteps.thy
--- 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}.