added an acknowledgement section
authorChristian Urban <urbanc@in.tum.de>
Sat, 14 Feb 2009 16:09:04 +0000
changeset 119 4536782969fa
parent 118 5f003fdf2653
child 120 c39f83d8daeb
added an acknowledgement section
CookBook/Intro.thy
CookBook/Recipes/Config.thy
CookBook/Recipes/ExternalSolver.thy
CookBook/Recipes/NamedThms.thy
CookBook/Recipes/StoringData.thy
CookBook/document/root.tex
cookbook.pdf
--- 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