diff -r 930b1308fd96 -r 8f73e80c8c6f ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Sun Oct 11 16:30:59 2009 +0200 +++ b/ProgTutorial/Intro.thy Sun Oct 11 22:45:29 2009 +0200 @@ -94,10 +94,10 @@ \end{isabelle} These boxes correspond to how code can be processed inside the interactive - environment of Isabelle. It is therefore easy to experiment with what is - displayed. However, for better readability we will drop the enclosing - \isacommand{ML}~@{text "\ \ \"} and just write: - + environment of Isabelle. It is therefore easy to experiment with the code + that is given in this tutorial. However, for better readability we will drop + the enclosing \isacommand{ML}~@{text "\ \ \"} and just + write: @{ML [display,gray] "3 + 4"} @@ -218,7 +218,7 @@ \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' - chapter and also contributed the material on @{ML_functor Named_Thms}. + chapter and also contributed the material on @{ML_funct Named_Thms}. \item {\bf Christian Sternagel} proofread the tutorial and made many improvemets to the text.