CookBook/Intro.thy
changeset 170 90bee31628dc
parent 167 3e30ea95c7aa
child 177 4e2341f6599d
--- a/CookBook/Intro.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/Intro.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -14,7 +14,7 @@
   examples included in the tutorial. The code is as far as possible checked
   against recent versions of Isabelle.  If something does not work, then
   please let us know. If you have comments, criticism or like to add to the
-  tutorial, feel free---you are most welcome! The tutorial is meant to be 
+  tutorial, please feel free---you are most welcome! The tutorial is meant to be 
   gentle and comprehensive. To achieve this we need your feedback. 
 *}
 
@@ -38,7 +38,7 @@
   part of the distribution of Isabelle):
 
   \begin{description}
-  \item[The Implementation Manual] describes Isabelle
+  \item[The Isabelle/Isar Implementation Manual] describes Isabelle
   from a high-level perspective, documenting both the underlying
   concepts and some of the interfaces. 
 
@@ -48,9 +48,9 @@
   now, but some  parts, particularly the chapters on tactics, are still 
   useful.
 
-  \item[The Isar Reference Manual] is also an older document that provides
-  material about Isar and its implementation. Some material in it
-  is still useful.
+  \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.
   \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, and then look at the solutions.
+
 *}
 
 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
@@ -126,17 +130,30 @@
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
-  He also wrote section \ref{sec:conversion}.
+  He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
 
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.
 
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
-  chapter and also contributed recipe \ref{rec:named}.
+  chapter and also contributed the material on @{text NamedThmsFun}.
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining
-  errors lies with me.
+  errors lies with me.\bigskip
+
+  {\Large\bf
+  This document is still in the process of being written! All of the
+  text is still under constructions. Sections and 
+  chapters that are under \underline{heavy} construction are marked 
+  with TBD.}
+
+  
+  \vfill
+  This document was compiled with:\\
+  \input{version}
 *}
 
+
+
 end
\ No newline at end of file