ProgTutorial/Intro.thy
changeset 264 311830b43f8f
parent 263 195c4444dff7
child 265 c354e45d80d2
--- a/ProgTutorial/Intro.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -128,7 +128,7 @@
 
 text {*
   One unpleasant aspect of any code development inside a larger system is that
-  one has to aim for a ``moving target''. The Isabelle system is no exception. Every 
+  one has to aim at a ``moving target''. The Isabelle system is no exception. Every 
   update lets potentially all hell break loose, because other developers have
   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   but taking the view that incompatible code changes are a fact of life 
@@ -195,7 +195,7 @@
   \begin{itemize}
   \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
   \simpleinductive-package and the code for the @{text
-  "chunk"}-antiquotation. He also wrote the first version of the chapter
+  "chunk"}-antiquotation. He also wrote the first version of this chapter
   describing the package and has been helpful \emph{beyond measure} with
   answering questions about Isabelle.