CookBook/Intro.thy
changeset 156 e8f11280c762
parent 153 c22b507e1407
child 162 3fb9f820a294
--- a/CookBook/Intro.thy	Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Intro.thy	Tue Mar 03 13:00:55 2009 +0000
@@ -50,7 +50,7 @@
 
   \item[The Isar Reference Manual] provides specification material (like grammars,
   examples and so on) about Isar and its implementation. It is currently in
-  the process of being updated.  .
+  the process of being updated.
   \end{description}
 
   Then of course there is:
@@ -60,7 +60,7 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  to learn from other people's code.
+  to learn from that code.
   \end{description}
 
 *}
@@ -108,6 +108,10 @@
   Further information or pointers to files.
   \end{readmore}
 
+  A few exercises a scattered around the text. Their solutions are given 
+  in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
+  to solve the exercises on your own.
+
 *}
 
 section {* Acknowledgements *}
@@ -115,7 +119,7 @@
 text {*
   Financial support for this tutorial was provided by the German 
   Research Council (DFG) under grant number URB 165/5-1. The following
-  people contributed:
+  people contributed to the text:
 
   \begin{itemize}
   \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the