--- 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 "\<verbopen> \<dots> \<verbclose>"} 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 "\<verbopen> \<dots> \<verbclose>"} 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.