diff -r 3e117bbf8316 -r 7b2625cea982 CookBook/document/root.bib
--- a/CookBook/document/root.bib	Fri Oct 10 17:09:17 2008 +0200
+++ b/CookBook/document/root.bib	Fri Oct 10 17:11:46 2008 +0200
@@ -1,10 +1,44 @@
+@Misc{Bornat-lecture,
+  author =	 {Richard Bornat},
+  title =	 {In defence of programming},
+  howpublished = {Available online via
+                  \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}},
+  month =	 {April},
+  year =	 2005,
+  note =	 {Corrected and revised version of inaugural lecture,
+                  delivered on 22nd January 2004 at the School of
+                  Computing Science, Middlesex University}
+}
 
-@manual{isa-imp,
-  author	= {Makarius Wenzel},
-  title		= {The {Isabelle/Isar} Implementation},
-  institution	= {Technische Universit\"at M\"unchen},
-  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+@inproceedings{Krauss-IJCAR06,
+  author =	 {Alexander Krauss},
+  title =	 {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic},
+  editor =	 {Ulrich Furbach and Natarajan Shankar},
+  booktitle =	 {Automated Reasoning, Third International Joint
+                  Conference, IJCAR 2006, Seattle, WA, USA, August
+                  17-20, 2006, Proceedings},
+  publisher =	 {Springer-Verlag},
+  series =	 {Lecture Notes in Computer Science},
+  volume =	 {4130},
+  year =	 {2006},
+  pages =	 {589-603}
+}
 
+@INPROCEEDINGS{Melham:1992:PIR,
+  AUTHOR =	 {T. F. Melham},
+  TITLE =	 {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in
+                  {HOL}},
+  BOOKTITLE =	 {Proceedings of the 1991 International Workshop on
+                  the {HOL} Theorem Proving System and its
+                  Applications, {D}avis, {C}alifornia, {A}ugust
+                  28--30, 1991},
+  EDITOR =	 {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt
+                  and Phillip J. Windley},
+  PUBLISHER =	 {IEEE Computer Society Press},
+  YEAR =	 {1992},
+  PAGES =	 {350--357},
+  ISBN =	 {0-8186-2460-4},
+}
 
 @Book{isa-tutorial,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
@@ -18,4 +52,77 @@
   title		= {{ML} for the Working Programmer},
   year		= 1996,
   edition	= {2nd},
-  publisher	= {Cambridge University Press}}
\ No newline at end of file
+  publisher	= {Cambridge University Press}}
+
+@InCollection{Paulson-ind-defs,
+  author =	 {L. C. Paulson},
+  title =	 {A fixedpoint approach to (co)inductive and
+                  (co)datatype definitions},
+  booktitle =	 {Proof, Language, and Interaction: Essays in Honour
+                  of Robin Milner},
+  pages =	 {187--211},
+  publisher =	 {MIT Press},
+  year =	 2000,
+  editor =	 {G. Plotkin and C. Stirling and M. Tofte}
+}
+
+@inproceedings{Schirmer-LPAR04,
+  author =	 {Norbert Schirmer},
+  title =	 {{A} {V}erification {E}nvironment for {S}equential {I}mperative
+                  Programs in {I}sabelle/{HOL}},
+  booktitle =	 "Logic for Programming, Artificial Intelligence, and
+                  Reasoning",
+  editor =	 "F. Baader and A. Voronkov",
+  year =	 2005,
+  publisher =	 "Springer-Verlag",
+  series =	 "Lecture Notes in Artificial Intelligence",
+  volume =	 3452,
+  pages =	 {398--414}
+}
+
+@TechReport{Schwichtenberg-MLCF,
+  author =	 {Helmut Schwichtenberg},
+  title =	 {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},
+  institution =	 {Mathematisches Institut,
+                  Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
+  year =	 2005,
+  month =	 {December},
+  note =	 {Available online at
+                  \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}}
+}
+
+@inproceedings{Urban-Berghofer06,
+  author =	 {Christian Urban and Stefan Berghofer},
+  title =	 {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes
+                  {I}mplemented in {I}sabelle/{HOL}},
+  editor =	 {Ulrich Furbach and Natarajan Shankar},
+  booktitle =	 {Automated Reasoning, Third International Joint
+                  Conference, IJCAR 2006, Seattle, WA, USA, August
+                  17-20, 2006, Proceedings},
+  publisher =	 {Springer-Verlag},
+  series =	 {Lecture Notes in Computer Science},
+  volume =	 {4130},
+  year =	 {2006},
+  pages =	 {498-512}
+}
+
+@inproceedings{Wadler-AFP95,
+  author =	 {Philip Wadler},
+  title =	 {Monads for Functional Programming},
+  pages =	 {24-52},
+  editor =	 {Johan Jeuring and Erik Meijer},
+  booktitle =	 {Advanced Functional Programming, First International
+                  Spring School on Advanced Functional Programming
+                  Techniques, B{\aa}stad, Sweden, May 24-30, 1995,
+                  Tutorial Text},
+  publisher =	 {Springer-Verlag},
+  series =	 {Lecture Notes in Computer Science},
+  volume =	 {925},
+  year =	 {1995}
+}
+
+@manual{isa-imp,
+  author	= {Makarius Wenzel},
+  title		= {The {Isabelle/Isar} Implementation},
+  institution	= {Technische Universit\"at M\"unchen},
+  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}