1.1 --- a/doc-src/manual.bib	Fri May 14 22:30:24 2010 +0200
     1.2 +++ b/doc-src/manual.bib	Fri May 14 22:43:00 2010 +0200
     1.3 @@ -228,13 +228,19 @@
     1.4  title="Introduction to Functional Programming using Haskell",
     1.5  publisher=PH,year=1998}
     1.6  
     1.7 -@inproceedings{blanchette-nipkow-2009,
     1.8 -  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
     1.9 +@inproceedings{blanchette-nipkow-2010,
    1.10 +  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
    1.11    author = "Jasmin Christian Blanchette and Tobias Nipkow",
    1.12 -  booktitle = "{TAP} 2009: Short Papers",
    1.13 -  editor = "Catherine Dubois",
    1.14 -  publisher = "ETH Technical Report 630",
    1.15 -  year = 2009}
    1.16 +  crossref = {itp2010}}
    1.17 +
    1.18 +@inproceedings{boehme-nipkow-2010,
    1.19 +  author={Sascha B\"ohme and Tobias Nipkow},
    1.20 +  title={Sledgehammer: Judgement Day},
    1.21 +  booktitle={Automated Reasoning: IJCAR 2010},
    1.22 +  editor={J. Giesl and R. H\"ahnle},
    1.23 +  publisher=Springer,
    1.24 +  series=LNCS,
    1.25 +  year=2010}
    1.26  
    1.27  @Article{boyer86,
    1.28    author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
    1.29 @@ -620,6 +626,11 @@
    1.30    pages =	 {203--220},
    1.31    crossref =     {tphols96}}
    1.32  
    1.33 +@misc{metis,
    1.34 +  author = "Joe Hurd",
    1.35 +  title = "Metis Theorem Prover",
    1.36 +  note = "\url{http://www.gilith.com/software/metis/}"}
    1.37 +
    1.38  %J
    1.39  
    1.40  @article{haskell-revised-report,
    1.41 @@ -1256,6 +1267,15 @@
    1.42    publisher	= {Addison-Wesley},
    1.43    year		= 1990}
    1.44  
    1.45 +@article{riazanov-voronkov-2002,
    1.46 +  author = "Alexander Riazanov and Andrei Voronkov",
    1.47 +  title = "The Design and Implementation of {Vampire}",
    1.48 +  journal = "Journal of AI Communications",
    1.49 +  year = 2002,
    1.50 +  volume = 15,
    1.51 +  number ="2/3",
    1.52 +  pages = "91--110"}
    1.53 +
    1.54  @book{Rosen-DMA,author={Kenneth H. Rosen},
    1.55  title={Discrete Mathematics and Its Applications},
    1.56  publisher={McGraw-Hill},year=1998}
    1.57 @@ -1287,6 +1307,15 @@
    1.58    number =       4
    1.59  }
    1.60  
    1.61 +@article{schulz-2002,
    1.62 +  author = "Stephan Schulz",
    1.63 +  title = "E---A Brainiac Theorem Prover",
    1.64 +  journal = "Journal of AI Communications",
    1.65 +  year = 2002,
    1.66 +  volume = 15,
    1.67 +  number ="2/3",
    1.68 +  pages = "111--126"}
    1.69 +
    1.70  @misc{sledgehammer-2009,
    1.71    key = "Sledgehammer",
    1.72    title = "The {S}ledgehammer: Let Automatic Theorem Provers
    1.73 @@ -1305,6 +1334,17 @@
    1.74    year		= 1972,
    1.75    publisher	= {Dover}}
    1.76  
    1.77 +@inproceedings{sutcliffe-2000,
    1.78 +  author = "Geoff Sutcliffe",
    1.79 +  title = "System Description: {SystemOnTPTP}",
    1.80 +  editor = "J. G. Carbonell and J. Siekmann",
    1.81 +  booktitle	= {Automated Deduction --- {CADE}-17 International Conference},
    1.82 +  series = "Lecture Notes in Artificial Intelligence",
    1.83 +  volume = {1831},
    1.84 +  pages = "406--410",
    1.85 +  year = 2000,
    1.86 +  publisher = Springer}
    1.87 +
    1.88  @InCollection{szasz93,
    1.89    author	= {Nora Szasz},
    1.90    title		= {A Machine Checked Proof that {Ackermann's} Function is not
    1.91 @@ -1411,6 +1451,11 @@
    1.92    note =	 {\url{http://x-symbol.sourceforge.net}}
    1.93  }
    1.94  
    1.95 +@misc{weidenbach-et-al-2009,
    1.96 +  author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
    1.97 +  title = "{SPASS} Version 3.5",
    1.98 +  note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
    1.99 +
   1.100  @manual{isabelle-sys,
   1.101    author	= {Markus Wenzel and Stefan Berghofer},
   1.102    title		= {The {Isabelle} System Manual},
   1.103 @@ -1750,6 +1795,14 @@
   1.104  %  editor        =
   1.105  %  volume        = 4732,
   1.106  
   1.107 +@Proceedings{itp2010,
   1.108 +  title         = {Interactive Theorem Proving: {ITP}-10},
   1.109 +  booktitle     = {Interactive Theorem Proving: {ITP}-10},
   1.110 +  editor = "Matt Kaufmann and Lawrence Paulson",
   1.111 +  publisher     = Springer,
   1.112 +  series        = LNCS,
   1.113 +  year          = 2010}
   1.114 +
   1.115  @unpublished{classes_modules,
   1.116    title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
   1.117    author        = {Stefan Wehr et. al.}