--- a/CookBook/document/root.bib	Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/document/root.bib	Wed Feb 18 17:17:37 2009 +0000
@@ -1,6 +1,6 @@
 @Misc{Bornat-lecture,
-  author =	 {Richard Bornat},
-  title =	 {In defence of programming},
+  author =	 {R.~Bornat},
+  title =	 {In {D}efence of {P}rogramming},
   howpublished = {Available online via
                   \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}},
   month =	 {April},
@@ -11,7 +11,7 @@
 }
 
 @inproceedings{Krauss-IJCAR06,
-  author =	 {Alexander Krauss},
+  author =	 {A.~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
@@ -25,7 +25,7 @@
 }
 
 @INPROCEEDINGS{Melham:1992:PIR,
-  AUTHOR =	 {T. F. Melham},
+  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
@@ -41,7 +41,7 @@
 }
 
 @Book{isa-tutorial,
-  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  author	= {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},
   title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
   publisher	= {Springer},
   year		= 2002,
@@ -55,7 +55,7 @@
   publisher	= {Cambridge University Press}}
 
 @InCollection{Paulson-ind-defs,
-  author =	 {L. C. Paulson},
+  author =	 {L.~C.~Paulson},
   title =	 {A fixedpoint approach to (co)inductive and
                   (co)datatype definitions},
   booktitle =	 {Proof, Language, and Interaction: Essays in Honour
@@ -67,7 +67,7 @@
 }
 
 @inproceedings{Schirmer-LPAR04,
-  author =	 {Norbert Schirmer},
+  author =	 {N.~Schirmer},
   title =	 {{A} {V}erification {E}nvironment for {S}equential {I}mperative
                   Programs in {I}sabelle/{HOL}},
   booktitle =	 "Logic for Programming, Artificial Intelligence, and
@@ -81,7 +81,7 @@
 }
 
 @TechReport{Schwichtenberg-MLCF,
-  author =	 {Helmut Schwichtenberg},
+  author =	 {H.~Schwichtenberg},
   title =	 {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},
   institution =	 {Mathematisches Institut,
                   Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
@@ -92,7 +92,7 @@
 }
 
 @inproceedings{Urban-Berghofer06,
-  author =	 {Christian Urban and Stefan Berghofer},
+  author =	 {C.~Urban and S.~Berghofer},
   title =	 {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes
                   {I}mplemented in {I}sabelle/{HOL}},
   editor =	 {Ulrich Furbach and Natarajan Shankar},
@@ -107,7 +107,7 @@
 }
 
 @inproceedings{Wadler-AFP95,
-  author =	 {Philip Wadler},
+  author =	 {P.~Wadler},
   title =	 {Monads for Functional Programming},
   pages =	 {24-52},
   editor =	 {Johan Jeuring and Erik Meijer},
@@ -122,7 +122,17 @@
 }
 
 @manual{isa-imp,
-  author	= {Makarius Wenzel},
+  author	= {M.~Wenzel},
   title		= {The {Isabelle/Isar} Implementation},
   institution	= {Technische Universit\"at M\"unchen},
   note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+
+@book{GordonMilnerWadsworth79,
+  author    = {M.~Gordon and R.~Milner and C.~P.~Wadsworth},
+  title     = {{E}dinburgh {LCF}},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {78},
+  year      = {1979}
+}
\ No newline at end of file