diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 2db8539..3ef8ad5 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -191,6 +191,11 @@ The OCAML website\\
 
 \section{Lisp to Hardware}
 
+\bibitem[Daly 10]{Daly10} Daly, Timothy\\
+``Intel Instruction Semantics Generator''\\
+\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/|
+\verb|intel/intel.pdf|
+
 \bibitem[Hardin 13]{Hard13} Hardin, David S.; McClurg, Jedidiah R.; 
 Davis, Jennifer A.\\
 ``Creating Formally Verified Components for Layered Assurance with an LLVM to ACL2 Translator''\\
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index fbe7ce1..e9bd176 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -4074,6 +4074,19 @@ exactly the mathematical dependencies between different structures.
 This may ease the achievement of proofs.
 \end{adjustwidth}
 
+\bibitem[Daly 10]{Daly10} Daly, Timothy\\
+``Intel Instruction Semantics Generator''\\
+\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/|
+\verb|intel/intel.pdf
+%\verb|axiom-developer.org/axiom-website/papers/Daly10.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Given an Intel x86 binary, extract the semantics of the instruction
+stream as Conditional Concurrent Assignments (CCAs). These CCAs 
+represent the semantics of each individual instruction. They can be
+composed to represent higher level semantics.
+\end{adjustwidth}
+
 \bibitem[Danielsson 06]{Dani06} Danielsson, Nils Anders; Hughes, John;
 Jansson, Patrik; Gibbons, Jeremy\\
 ``Fast and Loose Reasoning is Morally Correct''\\
diff --git a/changelog b/changelog
index 2e9af78..ea7ea0a 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20140724 tpd src/axiom-website/patches.html 20140724.02.tpd.patch
+20140724 tpd books/bookvol13 add Daly10 for proving Axiom
+20140724 tpd books/bookvolbib add Daly10 for proving Axiom
 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
diff --git a/patch b/patch
index 8cc42f3..5eb7093 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,13 @@
-books/bookvol13, bookvolbib add Mason86 for proving Axiom
+books/bookvol13, bookvolbib add Daly for proving Axiom
 
-\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[Daly 10]{Daly10} Daly, Timothy\\
+``Intel Instruction Semantics Generator''\\
+\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/|
+\verb|intel/intel.pamphlet|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Given an Intel x86 binary, extract the semantics of the instruction
+stream as Conditional Concurrent Assignments (CCAs). These CCAs 
+represent the semantics of each individual instruction. They can be
+composed to represent higher level semantics.
+\end{adjustwidth}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 7ba5568..c41f16f 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4562,6 +4562,8 @@ books/bookvol10.1 add section on interpolation formulas
 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
+<a href="patches/20140724.02.tpd.patch">20140724.02.tpd.patch</a>
+books/bookvol13, bookvolbib add Daly10 for proving Axiom
  </body>
 </html>