diff -r 26e5b41faa74 -r 79696161ae16 CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Feb 16 17:17:24 2009 +0000 +++ b/CookBook/Intro.thy Tue Feb 17 02:12:19 2009 +0000 @@ -15,7 +15,7 @@ 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 - gentle and comprehensive. + gentle and comprehensive. To achieve this we need your feedback. *} section {* Intended Audience and Prior Knowledge *} @@ -94,10 +94,10 @@ @{ML_response [display,gray] "3 + 4" "7"} - The usual user-level commands of Isabelle are written in bold, for - example \isacommand{lemma}, \isacommand{foobar} and so on. - We use @{text "$"} to indicate that a command needs to be run - in a Unix-shell, for example: + The user-level commands of Isabelle (i.e.~the non-ML code) are written + in bold, for example \isacommand{lemma}, \isacommand{apply}, + \isacommand{foobar} and so on. We use @{text "$"} to indicate that a + command needs to be run in a Unix-shell, for example: @{text [display] "$ ls -la"} @@ -114,13 +114,15 @@ text {* Financial support for this tutorial was provided by the German - Research Council (DFG) under grant number URB 165/5-1. + Research Council (DFG) under grant number URB 165/5-1. The following + people contributed: \begin{itemize} - \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the - \simpleinductive-package and the code for the @{text "chunk"}-antiquotation. He also wrote the first - version of the chapter describing the package and has be - helpful \emph{beyond measure} with answering questions about Isabelle. + \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the + \simpleinductive-package and the code for the @{text + "chunk"}-antiquotation. He also wrote the first version of the chapter + describing the package and has been helpful \emph{beyond measure} with + answering questions about Isabelle. \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}.