diff -r 195c4444dff7 -r 311830b43f8f ProgTutorial/Intro.thy --- 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.