# HG changeset patch # User Christian Urban # Date 1234627744 0 # Node ID 4536782969fa297b8811d2109149705132cbe83f # Parent 5f003fdf2653bd4943e64da4b7f1b655f2e1eb3c added an acknowledgement section diff -r 5f003fdf2653 -r 4536782969fa CookBook/Intro.thy --- 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 diff -r 5f003fdf2653 -r 4536782969fa CookBook/Recipes/Config.thy --- 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 {* diff -r 5f003fdf2653 -r 4536782969fa CookBook/Recipes/ExternalSolver.thy --- 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. diff -r 5f003fdf2653 -r 4536782969fa CookBook/Recipes/NamedThms.thy --- 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 {* diff -r 5f003fdf2653 -r 4536782969fa CookBook/Recipes/StoringData.thy --- 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 {* diff -r 5f003fdf2653 -r 4536782969fa CookBook/document/root.tex --- 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\\ diff -r 5f003fdf2653 -r 4536782969fa cookbook.pdf Binary file cookbook.pdf has changed