diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index b1f6ddd..2db8539 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -201,6 +201,10 @@ Greve, David A.; McClurg, Jedidiah R.\\
 ``Development of a Translator from LLVM to ACL2''\\
 \verb|arxiv.org/pdf/1406.1566|
 
+\bibitem[Mason 86]{Mason86} Mason, Ian A.\\
+``The Semantics of Destructive Lisp''\\
+Center for the Study of Language and Information ISBN 0-937073-06-7
+
 \bibitem[Wiki 14a]{Wiki14a} ProofWiki\\
 ``Euclidean Algorithm''\\
 \verb|proofwiki.org/wiki/Euclidean_Algorithm|
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 9e58092..fbe7ce1 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -4275,6 +4275,10 @@ validation test for that example.
 Addison-Wesley ISBN 0-321-14306-X
 %\verb|axiom-developer.org/axiom-website/papers/Lamp02.pdf|
 
+\bibitem[Mason 86]{Mason86} Mason, Ian A.\\
+``The Semantics of Destructive Lisp''\\
+Center for the Study of Language and Information ISBN 0-937073-06-7
+
 \bibitem[Newcombe 13]{Newc13} Newcombe, Chris; Rath, Tim; Zhang, Fan;
 Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael\\
 ``Use of Formal Methods at Amazon Web Services''\\
diff --git a/changelog b/changelog
index 86828d5..2e9af78 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20140724 tpd src/axiom-website/patches.html 20140724.01.tpd.patch
+20140724 tpd books/bookvol13 add Mason86 for proving Axiom
+20140724 tpd books/bookvolbib add Mason86 for proving Axiom
 20140723 tpd src/axiom-website/patches.html 20140723.01.tpd.patch
 20140723 tpd books/bookvol10.1 expand section on interpolation formulas
 20140723 tpd books/bookvolbib update reference for Ham62
diff --git a/patch b/patch
index 4ccdbe9..8cc42f3 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,5 @@
-books/bookvol10.1, bookvolbib expand section on interpolation formulas
+books/bookvol13, bookvolbib add Mason86 for proving Axiom
 
-Show a common structure for constructing interpolation formulas.
+\bibitem[Mason 86]{Mason86} Mason, Ian A.\\
+``The Semantics of Destructive Lisp''\\
+Center for the Study of Language and Information ISBN 0-937073-06-7
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 664174d..7ba5568 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4560,6 +4560,8 @@ books/bookvol7, bookvol8 apply Camm's patches
 books/bookvol10.1 add section on interpolation formulas
 <a href="patches/20140723.01.tpd.patch">20140723.01.tpd.patch</a>
 books/bookvol10.1 expand section on interpolation formulas
+<a href="patches/20140724.01.tpd.patch">20140724.01.tpd.patch</a>
+books/bookvol13, bookvolbib add Mason86 for proving Axiom
  </body>
 </html>