--- a/CookBook/Intro.thy Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Intro.thy Sat Feb 14 16:09:04 2009 +0000
@@ -109,5 +109,30 @@
*}
+section {* Acknowledgements *}
+
+text {*
+ Financial support for this tutorial was provided by the German
+ Research Council (DFG) under grant number URB 165/5-1.
+
+ \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 generally be
+ helpful 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}.
+
+ \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}.
+ \end{itemize}
+
+ Please let me know if I forgotten anything. All errors are of course my
+ resposibility.
+*}
end
\ No newline at end of file
--- a/CookBook/Recipes/Config.thy Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Recipes/Config.thy Sat Feb 14 16:09:04 2009 +0000
@@ -2,7 +2,7 @@
imports "../Base"
begin
-section {* Configuration Options *}
+section {* Configuration Options\label{rec:config} *}
text {*
--- a/CookBook/Recipes/ExternalSolver.thy Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy Sat Feb 14 16:09:04 2009 +0000
@@ -4,7 +4,7 @@
begin
-section {* Executing an External Application *}
+section {* Executing an External Application \label{rec:external}*}
text {*
{\bf Problem:}
@@ -57,9 +57,11 @@
-section {* Writing an Oracle\label{rec:external} *}
+section {* Writing an Oracle\label{rec:oracle} *}
text {*
+ (FIXME: should go into a separate file)
+
{\bf Problem:}
You want to use a fast, new decision procedure not based one Isabelle's
tactics, and you do not care whether it is sound.
--- a/CookBook/Recipes/NamedThms.thy Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy Sat Feb 14 16:09:04 2009 +0000
@@ -2,7 +2,7 @@
imports "../Base"
begin
-section {* Accumulate a List of Theorems under a Name *}
+section {* Accumulate a List of Theorems under a Name\label{rec:named} *}
text {*
--- a/CookBook/Recipes/StoringData.thy Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy Sat Feb 14 16:09:04 2009 +0000
@@ -2,7 +2,7 @@
imports "../Base"
begin
-section {* Storing Data\label{recipe:storingdata} *}
+section {* Storing Data\label{rec:storingdata} *}
text {*
--- a/CookBook/document/root.tex Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/document/root.tex Sat Feb 14 16:09:04 2009 +0000
@@ -123,9 +123,9 @@
\title{\mbox{}\\[-10ex]
\includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
- The Isabelle Programming Tutorial (fragment)}
+ The Isabelle Programming Tutorial (draft)}
-\author{with contributions by:\\[2ex]
+\author{by Christian Urban with contributions from:\\[2ex]
\begin{tabular}{r@{\hspace{1.8mm}}l}
Stefan & Berghofer\\
Sascha & Böhme\\
Binary file cookbook.pdf has changed