diff -r b6fca043a796 -r e8f11280c762 CookBook/Intro.thy --- 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