diff -r 95461cf6fd07 -r 5fc2fb34c323 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Fri Jan 01 00:19:11 2010 +0100 +++ b/ProgTutorial/Intro.thy Fri Jan 08 21:31:45 2010 +0100 @@ -40,7 +40,7 @@ operating system or editor in which Isabelle is used. If you have comments, criticism or like to add to the tutorial, please feel free---you are most welcome! The tutorial is meant to be gentle and comprehensive. To achieve - this we need your feedback. + this we need your help and feedback. *} section {* Intended Audience and Prior Knowledge *} @@ -62,8 +62,8 @@ \begin{description} \item[The Isabelle/Isar Implementation Manual] describes Isabelle - from a high-level perspective, documenting both the underlying - concepts and some of the interfaces. + from a high-level perspective, documenting some of the underlying + concepts and interfaces. \item[The Isabelle Reference Manual] is an older document that used to be the main reference of Isabelle at a time when all proof scripts @@ -84,8 +84,8 @@ good to look at code that does similar things as you want to do and learn from it. This tutorial contains frequently pointers to the Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is - often your best friend while programming with Isabelle, or - hypersearch if you program using jEdit under MacOSX. To understand the sources, + often your best friend while programming with Isabelle.\footnote{Or + hypersearch if you program using jEdit under MacOSX.} To understand the sources, it is often also necessary to track the change history of a file or files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} for Isabelle provides convenient interfaces to query the history of @@ -136,8 +136,9 @@ \end{readmore} The pointers to Isabelle files are hyperlinked to the tip of the Mercurial - repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/} - {http://isabelle.in.tum.de/repos/isabelle/}. + repository at \href{http://isabelle.in.tum.de/repos/isabelle/} + {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release + of Isabelle. A few exercises are scattered around the text. Their solutions are given in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try @@ -216,9 +217,9 @@ \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 this chapter - describing the package and has been helpful \emph{beyond measure} with - answering questions about Isabelle. + "chunk"}-antiquotation. He also wrote the first version of chapter + \ref{chp:package} describing this package and has been helpful \emph{beyond + measure} with answering questions about Isabelle. \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. @@ -227,15 +228,15 @@ and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} are by him. - \item {\bf Lukas Bulwahn} made me aware of the problems with recursive + \item {\bf Lukas Bulwahn} made me aware of a problem with recursive parsers and contributed exercise \ref{ex:contextfree}. - \item {\bf Jeremy Dawson} wrote the first version of the chapter + \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing} about parsing. \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. - \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' + \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' chapter and also contributed the material on @{ML_funct Named_Thms}. \item {\bf Christian Sternagel} proofread the tutorial and made