src/HOL/Extraction/document/root.bib

+@Article{Berger-JAR-2001,
+  author =       {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger},
+  title =        {The {Warshall} Algorithm and {Dickson's} Lemma: Two
+                  Examples of Realistic Program Extraction},
+  journal =      {Journal of Automated Reasoning},
+  publisher =    {Kluwer Academic Publishers},
+  year =         2001,
+  volume =       26,
+  pages =        {205--221}
+}
+
+@TechReport{Coquand93,
+  author = 	 {Thierry Coquand and Daniel Fridlender},
+  title = 	 {A proof of {Higman's} lemma by structural induction},
+  institution =  {Chalmers University},
+  year = 	 1993,
+  month =	 {November}
+}