--- 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.