diff -r d1c9bf0f8ae8 -r fe3c65d9c577 doc-src/manual.bib
--- a/doc-src/manual.bib	Thu Oct 22 09:50:29 2009 +0200
+++ b/doc-src/manual.bib	Thu Oct 22 14:45:20 2009 +0200
@@ -49,7 +49,7 @@
 
 @Unpublished{abrial93,
   author	= {J. R. Abrial and G. Laffitte},
-  title		= {Towards the Mechanization of the Proofs of some Classical
+  title		= {Towards the Mechanization of the Proofs of Some Classical
 		  Theorems of Set Theory},
   note		= {preprint},
   year		= 1993,
@@ -73,6 +73,17 @@
   crossref	= {types93},
   pages		= {213-237}}
 
+@inproceedings{andersson-1993,
+  author = "Arne Andersson",
+  title = "Balanced Search Trees Made Simple",
+  editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
+  booktitle = "WADS 1993",
+  series = LNCS,
+  volume = {709},
+  pages = "61--70",
+  year = 1993,
+  publisher = Springer}
+
 @book{andrews86,
   author	= "Peter Andrews",
   title		= "An Introduction to Mathematical Logic and Type Theory: to Truth
@@ -167,6 +178,15 @@
   author          = "Stefan Berghofer and Tobias Nipkow",
   pages           = "38--52"}
 
+@inproceedings{berghofer-nipkow-2004,
+  author = {Stefan Berghofer and Tobias Nipkow},
+  title = {Random Testing in {I}sabelle/{HOL}},
+  pages = {230--239},
+  editor = "J. Cuellar and Z. Liu",
+  booktitle = {{SEFM} 2004},
+  publisher = IEEE,
+  year = 2004}
+
 @InProceedings{Berghofer-Nipkow:2002,
   author =       {Stefan Berghofer and Tobias Nipkow},
   title =        {Executing Higher Order Logic},
@@ -200,6 +220,14 @@
 title="Introduction to Functional Programming using Haskell",
 publisher=PH,year=1998}
 
+@inproceedings{blanchette-nipkow-2009,
+  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
+  author = "Jasmin Christian Blanchette and Tobias Nipkow",
+  booktitle = "{TAP} 2009: Short Papers",
+  editor = "Catherine Dubois",
+  publisher = "ETH Technical Report 630",
+  year = 2009}
+
 @Article{boyer86,
   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
 		   Overbeek and Mark Stickel and Lawrence Wos},
@@ -241,7 +269,7 @@
 }
 
 @InProceedings{bulwahn-et-al:2008:imperative,
-  author   = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
+  author   = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
   title    = {Imperative Functional Programming with {Isabelle/HOL}},
   crossref = {tphols2008},
 }
@@ -597,6 +625,12 @@
   year =    2003,
   note =    {\url{http://www.haskell.org/definition/}}}
 
+@book{jackson-2006,
+  author = "Daniel Jackson",
+  title = "Software Abstractions: Logic, Language, and Analysis",
+  publisher = MIT,
+  year = 2006}
+
 %K
 
 @InProceedings{kammueller-locales,
@@ -878,10 +912,11 @@
 
 @Book{isa-tutorial,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
-  title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
-  publisher	= {Springer},
+  title		= {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
+  publisher	= Springer,
   year		= 2002,
-  note		= {LNCS Tutorial 2283}}
+  series    = LNCS,
+  volume    = 2283}
 
 @Article{noel,
   author	= {Philippe No{\"e}l},
@@ -1021,7 +1056,7 @@
                    Essays in Honor of {Robin Milner}},
   booktitle	= {Proof, Language, and Interaction: 
                    Essays in Honor of {Robin Milner}},
-  publisher	= {MIT Press},
+  publisher	= MIT,
   year		= 2000,
   editor	= {Gordon Plotkin and Colin Stirling and Mads Tofte}}
 
@@ -1236,6 +1271,12 @@
   number =       4
 }
 
+@misc{sledgehammer-2009,
+  key = "Sledgehammer",
+  title = "The {S}ledgehammer: Let Automatic Theorem Provers
+Write Your {I}s\-a\-belle Scripts",
+  note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
+
 @inproceedings{slind-tfl,
   author	= {Konrad Slind},
   title		= {Function Definition in Higher Order Logic},
@@ -1295,6 +1336,27 @@
 title={Haskell: The Craft of Functional Programming},
 publisher={Addison-Wesley},year=1999}
 
+@misc{kodkod-2009,
+  author = "Emina Torlak",
+  title = {Kodkod: Constraint Solver for Relational Logic},
+  note = "\url{http://alloy.mit.edu/kodkod/}"}
+
+@misc{kodkod-2009-options,
+  author = "Emina Torlak",
+  title = "Kodkod {API}: Class {Options}",
+  note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
+
+@inproceedings{torlak-jackson-2007,
+  title = "Kodkod: A Relational Model Finder",
+  author = "Emina Torlak and Daniel Jackson",
+  editor = "Orna Grumberg and Michael Huth",
+  booktitle = "TACAS 2007",
+  series = LNCS,
+  volume = {4424},
+  pages = "632--647",
+  year = 2007,
+  publisher = Springer}
+
 @Unpublished{Trybulec:1993:MizarFeatures,
   author = 	 {A. Trybulec},
   title = 	 {Some Features of the {Mizar} Language},
@@ -1320,6 +1382,13 @@
   year          = 1989
 }
 
+@phdthesis{weber-2008,
+  author = "Tjark Weber",
+  title = "SAT-Based Finite Model Generation for Higher-Order Logic",
+  school = {Dept.\ of Informatics, T.U. M\"unchen},
+  type = "{Ph.D.}\ thesis",
+  year = 2008}
+
 @Misc{x-symbol,
   author =	 {Christoph Wedler},
   title =	 {Emacs package ``{X-Symbol}''},
@@ -1570,7 +1639,7 @@
 			Essays in Honor of {Larry Wos}},
   booktitle	= {Automated Reasoning and its Applications: 
 			Essays in Honor of {Larry Wos}},
-  publisher	= {MIT Press},
+  publisher	= MIT,
   year		= 1997,
   editor	= {Robert Veroff}}
 
@@ -1669,3 +1738,8 @@
   title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
   author        = {Stefan Wehr et. al.}
 }
+
+@misc{wikipedia-2009-aa-trees,
+  key = "Wikipedia",
+  title = "Wikipedia: {AA} Tree",
+  note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}