diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 90f2893..7d73944 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -577,10 +577,31 @@ Algorithms Group, Inc., Downer's Grove, IL, USA and Oxford, UK, December 1992.
Dunstan, Martin, Kelsey, Tom, Linton, Steve, Martin, Ursula
``Lightweight Formal Methods For Computer Algebra Systems''
\verb|www.cs.st-andrews.ac.uk/~tom/pub/issac98.pdf|
+\bibitem[Dun97]{Dun97}
+Dunstand, U, Linton
+``Embedded Verification Techniques for Computer Algebra Systems''
+Grant citation GR/L48256 Nov 1, 1997-Feb 28, 2001
+\verb|www.cs.st-andrews.ac.uk/research/output/detail?output=ML97.php|
\bibitem[Dun99]{Dun99}
``Formal Methods for Extensions to CAS''
Dunstan, Martin, Kelsey, Tom, Martin, Ursula, and Linton, Steve,
-FME 99, Toulouse, France, Sept 20-24, 1999
+FM 99, Toulouse, France, Sept 20-24, 1999, p1758-1777
+\bibitem[Dun99a]{Dun99a}
+Dunstan, MN
+``Larch/Aldor - A Larch BISL for AXIOM and Aldor''
+PhD Thesis, 1999
+\verb|www.cs.st-andrews.uk/files/publications/Dun99.php|
+\verb|axiom-portal.newsynthesis.org/refs/articles/mnd-sep99-thesis.pdf|
+\bibitem[DGKM01]{DGKM01}
+Dunstan, Martin, Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Computer Algebra meets Automated Theorem Proving: A Maple-PVS Interface''
+TPHOLS 2001, Edinburgh
+\verb|www.cs-st-andrews.ac.uk/~tom/pub/tphols.ps|
+\bibitem[DGKM01a]{DGKM01a}
+Dunstan, Martin, Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Computer Algebra meets Automated Theorem Proving: A Maple-PVS Interface''
+Calculemus 2001, Siena
+\verb|www.cs-st-andrews.ac.uk/~tom/pub/dunstanetal.ps|
\bibitem[Du95]{Du95}
Duval, D. ``Evaluation dynamique et cl\^oture alg\'ebrique en Axiom''.
Journal of Pure and Applied Algebra, no99, 1995, pp. 267--295.
@@ -640,6 +661,15 @@ material and energy balance concepts''. In Anonymous [Ano91], pp345-349
V. Ellen Golden and M. A. Hussain, editors. Proceedings of the 1984 MACSYMA
Users' Conference: Schenectady, New York, July 23-25, 1984, General Electric,
Schenectady, NY, USA, 1984
+\bibitem[GKM05]{GKM05}
+Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula
+``Hidden verification for computational mathematics''
+Journal of Symbolic Computation, Vol39, Num 5, 2005
+\bibitem[BHGM04]{BHGM04}
+Boulton, Richard, Hardy, Ruth, Gottliebsen, Hanne, and Martin, Ursula
+``Design verification for control engineering''
+Proc Fourth International Conference on Integrated Formal Methods,
+April 2004
\bibitem[GHK91]{GHK91}
J. Grabmeier, K. Huber, and U. Krieger. ``Das ComputeralgebraSystem AXIOM
bei kryptologischen und verkehrstheoretischen Untersuchungen des
@@ -807,6 +837,11 @@ Kelsey, Tom
``Formal specification of computer algebra''
University of St Andrews, 6th April 2000
\verb|www.cs.st-andrews.cs.uk/~tom/pub/fscbs.ps|
+\bibitem[Kel00b]{Kel00b}
+Kelsey, Tom
+``Formal specification of computer algebra'' (slides)
+University of St Andrews, Sept 21, 2000
+\verb|www.cs.st-andrews.cs.uk/~tom/pub/fscbstalk.ps|
\bibitem[Kel99]{Kel99}
Kelsey, Tom
``Formal Methods and Computer Algebra: A Larch Specification of AXIOM
diff --git a/changelog b/changelog
index 8edcce1..6f213a0 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20111208 tpd src/axiom-website/patches.html 20111208.05.tpd.patch
+20111208 tpd books/bookvolbib add additional references
20111208 tpd src/axiom-website/patches.html 20111208.04.tpd.patch
20111208 tpd books/bookvol9 code cleanup
20111208 tpd src/axiom-website/patches.html 20111208.03.tpd.patch
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 57e0f15..851ed6f 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -3733,5 +3733,7 @@ src/axiom-website/documentation update contributor list
books/bookvol5 treeshake interpreter
20111208.04.tpd.patch
books/bookvol9 code cleanup
+20111208.05.tpd.patch
+books/bookvolbib add additional references