diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 953e427..1211f8e 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -3156,5 +3156,24 @@ The first and second algorithms are deterministic, the third is
 probabilistic.
 \end{adjustwidth}
 
+\subsection{Proving Axiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\
+``Interactive Theorem Proving and Program Development''\\
+Springer ISBN 3-540-20854-2
+
+\begin{adjustwidth}{2.5em}{0pt}
+Coq is an interactive proof assistant for the development of
+mathematical theories and formally certified software. It is based on
+a theory called the calculus of inductive constructions, a variant of
+type theory.
+
+This book provides a pragmatic introduction to the development of
+proofs and certified programs using Coq. With its large collection of
+examples and exercies it is an invaluable tool for researchers,
+students, and engineers interested in formal methods and the
+development of zero-fault software.
+\end{adjustwidth}
+
 \end{thebibliography}
 \end{document}
diff --git a/changelog b/changelog
index 6086a6d..8655cec 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140612 tpd src/axiom-website/patches.html 20140612.01.tpd.patch
+20140612 tpd books/bookvolbib add Proving Axiom Correct section, Bert04
 20140610 tpd src/axiom-website/patches.html 20140610.05.tpd.patch
 20140610 tpd books/bookvolbib add Le96a
 20140610 tpd src/axiom-website/patches.html 20140610.04.tpd.patch
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index d0a13ce..69f7e69 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4418,6 +4418,8 @@ book/*.txt email cleanup
 books/bookvol10.4,bookvol5 add reportInstantiations to API package
 <a href="patches/20140610.05.tpd.patch">20140610.05.tpd.patch</a>
 books/bookvolbib add Le96a
+<a href="patches/20140612.01.tpd.patch">20140612.01.tpd.patch</a>
+books/bookvolbib add Proving Axiom Correct section, Bert04
  </body>
 </html>