ProgTutorial/Intro.thy
changeset 343 8f73e80c8c6f
parent 335 163ac0662211
child 346 0fea8b7a14a1
--- 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.