--- a/Paper/document/root.bib	Tue Mar 30 17:55:46 2010 +0200
+++ b/Paper/document/root.bib	Tue Mar 30 21:15:13 2010 +0200
@@ -2,19 +2,18 @@
   author = 	 {S.~Berghofer and M.~Wenzel},
   title = 	 {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in 
                   {F}ormal-{L}ogic {E}ngineering},
-  booktitle = 	 {Proc.~of the 12th International Conference Theorem Proving in 
-                  Higher Order Logics (TPHOLs)},
+  booktitle = 	 {Proc.~of the 12th TPHOLs conference},
   pages = 	 {19--36},
   year = 	 1999,
-  number = 	 1690,
+  volume = 	 1690,
   series = 	 {LNCS}
 }
 
 @InProceedings{CoreHaskell,
   author = 	 {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},
   title = 	 {{S}ystem {F} with {T}ype {E}quality {C}oercions},
-  booktitle = 	 {Proc of TLDI},
-  pages = 	 {??},
+  booktitle = 	 {Proc of the TLDI Workshop},
+  pages = 	 {53-66},
   year = 	 {2007}
 }
 
@@ -83,8 +82,8 @@
 @Unpublished{HuffmanUrban10,
   author = 	 {B.~Huffman and C.~Urban},
   title = 	 {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
-  note = 	 {To appear at {\it ITP'10 Conference}},
-  annote =       {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
+  note = 	 {To appear at {\it ITP'10 Conference}, 
+                  http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
   year = 	 {2010}
 }