doc-src/manual.bib

   publisher	= {Addison-Wesley},
   year		= 1990}
 
 @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,
   month		= Feb}
 

 @InProceedings{alf,
   author	= {Lena Magnusson and Bengt {Nordstr\"{o}m}},
   title		= {The {ALF} Proof Editor and Its Proof Engine},
   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
 through Proof",

   crossref        = "tphols2000",
   title           = "Proof terms for simply typed higher order logic",
   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},
   booktitle =    {Types for Proofs and Programs: TYPES'2000},
   editor =       {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},

 title="Introduction to Functional Programming",publisher=PH,year=1988}
 
 @book{Bird-Haskell,author="Richard Bird",
 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},
   title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}

   crossref = {tphols2007},
   pages    = {38--53}
 }
 
 @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},
 }
 %  pages    = {38--53}
 

   number =  1,
   pages =   {0--255},
   month =   {Jan},
   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,
   author = 	 {Florian Kamm{\"u}ller and Markus Wenzel and 

   year =         1993
 }
 
 @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},
   title		= {Experimenting with {Isabelle} in {ZF} Set Theory},
   journal	= JAR,

 @book{milner-fest,
   title		= {Proof, Language, and Interaction: 
                    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}}
 
 @InCollection{paulson-handbook,
   author	= {Lawrence C. Paulson},

   year =         1984,
   volume =       49,
   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},
   crossref  = {tphols96},
   pages		= {381-397}}

 
 @book{Thompson-Haskell,author={Simon Thompson},
 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},
   note = 	 {Presented at a workshop in Turin, Italy},
   year =	 1993

   author        = {P. Wadler and S. Blott},
   title         = {How to make ad-hoc polymorphism less ad-hoc},
   booktitle     = {ACM Symp.\ Principles of Programming Languages},
   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}''},
   note =	 {\url{http://x-symbol.sourceforge.net}}

 @book{wos-fest,
   title		= {Automated Reasoning and its Applications: 
 			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}}
 
 @proceedings{fme93,
   editor	= {J. C. P. Woodcock and P. G. Larsen},

 
 @unpublished{classes_modules,
   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}"}