diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index f6a7d06..ef026fe 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -1889,19 +1889,6 @@ Oxford University Press (2000) ISBN0-19-512516-9
``Literate Programming Tools Implemented in ANSI Common Lisp''\\
\verb|brlcad.org/~starseeker/cl-web-v0.8.lisp.pamphlet|
-\bibitem[Youssef 04]{You04} Youssef, Saul\\
-``Prospects for Category Theory in Aldor''\\
-October 2004\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
-\begin{adjustwidth}{2.5em}{0pt}
-Ways of encorporating category theory constructions and results into
-the Aldor language are discussed. The main features of Aldor which
-make this possible are identified, examples of categorical
-constructions are provided and a suggestion is made for a foundation
-for rigorous results.
-\end{adjustwidth}
-
\bibitem[Yun 83]{Yun83} Yun, David Y.Y.\\
``Computer Algebra and Complex Analysis''\\
Computational Aspects of Complex Analysis pp379-393
@@ -3492,10 +3479,6 @@ Math. Tables Aids Comput. 10 91--96. (1956)
\subsection{Y} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\bibitem[Youssef 04]{REF-You04} Youssef, Saul\\
-``Prospects for Category Theory in Aldor'' October 2004\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
\bibitem[Yun 76]{Yu76} Yun, D.Y.Y.\\
``On square-free decomposition algorithms''\\
{\sl Proceedings of SYMSAC'76} pages 26-35, 1976
@@ -3708,6 +3691,32 @@ symmetric monodial category''. We assume no prior knowledge of
category theory, proof theory or computer science.
\end{adjustwidth}
+\bibitem[Meijer 91]{Meij91} Meijer, Erik; Fokkinga, Maarten; Paterson, Ross\\
+``Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire''\\
+\verb|eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We develop a calculus for lazy functional programming based on
+recursion operators associated with data type definitions. For these
+operators we derive various algebraic laws that are useful in deriving
+and manipulating programs. We shall show that all example functions in
+Bird and Wadler's ``Introduction to Functional Programming'' can be
+expressed using these operators.
+\end{adjustwidth}
+
+\bibitem[Youssef 04]{You04} Youssef, Saul\\
+``Prospects for Category Theory in Aldor''\\
+October 2004\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Ways of encorporating category theory constructions and results into
+the Aldor language are discussed. The main features of Aldor which
+make this possible are identified, examples of categorical
+constructions are provided and a suggestion is made for a foundation
+for rigorous results.
+\end{adjustwidth}
+
\subsection{Proving Axiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\
@@ -4175,5 +4184,11 @@ from a technical question to a question of effectively capturing ideas.
In particular, this applies well to Axiom's focus on literate programming.
\end{adjustwidth}
+\subsection{Differential Equations} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\bibitem[Von Mohrenschildt 94]{Mohr94} Von Mohrenschildt, Martin\\
+``Symbolic Solutions of Discontinuous Differential Equations''\\
+\verb|e-collection.library.ethz.ch/eserv/eth:39463/eth-39463-01.pdf|
+
\end{thebibliography}
\end{document}
diff --git a/changelog b/changelog
index 58acd41..ea115e6 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140706 tpd src/axiom-website/patches.html 20140706.01.tpd.patch
+20140706 tpd books/bookvolbib add references Meij91, Mohr94
20140703 tpd src/axiom-website/patches.html 20140703.04.tpd.patch
20140703 tpd books/bookvolbib add Lamport book "Specifying Systems"
20140703 tpd src/axiom-website/patches.html 20140703.03.tpd.patch
diff --git a/patch b/patch
index 906da1e..1fc67d4 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,7 @@
-books/bookvolbib add Lamport book "Specifying Systems"
+books/bookvolbib add references Meij91, Mohr94
+
+Mohr94 is related to differential equations.
+Meij91 is related to category theory.
+
+
-Free pdf describing TLA+ model checking software.
-http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
-Part of the effort to begin proving Axiom correct.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index b954f24..8de3b19 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4526,6 +4526,8 @@ books/bookvolbib add Numerical Algorithms section, add Yang14
src/axiom-website/documentation.html add Lamport quote
20140703.04.tpd.patch
books/bookvolbib add Lamport book "Specifying Systems"
+20140706.01.tpd.patch
+books/bookvolbib add references Meij91, Mohr94