From 5569fc139e81c8d3f59eb65d7ead53e863b954bf Mon Sep 17 00:00:00 2001
From: Tim Daly <daly@axiom-developer.org>
Date: Thu, 29 Jan 2015 18:00:12 -0500
Subject: books/bookvol13 add Lamport 21st Century Proofs paper

---
 books/bookvol13.pamphlet       |    8 +++++++
 books/bookvolbib.pamphlet      |   41 ++++++++++++++++++++++++++++++++++++++++
 changelog                      |    2 +
 patch                          |   10 +--------
 src/axiom-website/patches.html |    2 +
 5 files changed, 54 insertions(+), 9 deletions(-)

diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 95a403a..9d3d770 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -237,6 +237,14 @@ let rec gcd a b = if b = 0 then a else gcd b (a mod b)
 val gcd : int -> int -> int = <fun>
 \end{verbatim}
 
+Leslie Lamport\cite{Lamp14} on $21^{st}$ Century Proofs.
+
+A method of writing proofs is described that makes it harder to prove
+things that are not true. The method, based on hierarchical
+structuring, is simple and practical. The author's twenty years of
+experience writing such proofs is discussed.
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Bibliography}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index b03e79e..5051fa5 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2833,6 +2833,47 @@ FME'99, Toulouse, France, Sept 20-24, 1999, pp 1758-1777
 
 \end{chunk}
 
+\index{Lamport, Leslie}
+\begin{chunk}{axiom.bib}
+@misc{Lamp13,
+  author = "Lamport, Leslie",
+  title = "Errata to Specifying Systems",
+  year = "2013",
+  url = "http://research.microsoft.com/en-us/um/people/lamport/tla/errata-1.pdf",
+  publisher = "Microsoft",
+  paper = "Lamp13.pdf",
+  abstract = "
+    These are all the errors and omissions to the first printing (July
+    2002) of the book {\sl Specifying Systems} reported as of 29 October
+    2013.  Positions in the book are indicated by page and line number,
+    where the top line of a page is number 1 and the bottom line is number
+    $-1$. A running head and a page number are not considered to be lines,
+    but all other lines are. Please report any additional errors to the
+    author, whose email address is posted on {\tt http://lamport.org}. The
+    first person to report an error will be acknowledged in any revised
+    edition."
+}
+
+\end{chunk}
+
+\index{Lamport, Leslie}
+\begin{chunk}{axiom.bib}
+@misc{Lamp14,
+  author = "Lamport, Leslie",
+  title = "How to Write a $21^{st}$ Century Proof",
+  year = "2014",
+  url = "http://research.microsoft.com/en-us/um/people/lamport/pubs/paper.pdf",
+  publisher = "Microsoft",
+  paper = "Lamp14.pdf",
+  abstract = "
+   A method of writing proofs is described that makes it harder to prove
+   things that are not true. The method, based on hierarchical
+   structuring, is simple and practical. The author's twenty years of
+   experience writing such proofs is discussed."
+}
+
+\end{chunk}
+
 \index{Martin, Ursula}
 \index{Shand, D.}
 \begin{chunk}{ignore}
diff --git a/changelog b/changelog
index 745cc8e..9f086a5 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20150129 tpd src/axiom-website/patches.html 20150129.01.tpd.patch
+20150129 tpd books/bookvol13 add Lamport 21st Century Proofs paper
 20150126 tpd src/axiom-website/patches.html 20150126.03.tpd.patch
 20150126 tpd buglist: bug 7299: docker image does not contain GCC
 20150126 wxh src/axiom-website/patches.html 20150126.02.wxh.patch
diff --git a/patch b/patch
index 02f228f..09b6421 100644
--- a/patch
+++ b/patch
@@ -1,10 +1,2 @@
-buglist: bug 7299: docker image does not contain GCC
-
-example from bookvol0:
-
-p(10)
-  Compiling function p with type Integer -> Polynomial(Fraction(Integer))
-  Compiling function p as a recurrence relation
-
-sh: 1: gcc: not found
+books/bookvol13 add Lamport 21st Century Proofs paper
 
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 7e834df..08a952f 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4980,6 +4980,8 @@ books/bookvol10.3 fixed bug 7297: Extraneous "#\" characters<br/>
 bookvol10.4 MLIFT bug 7298: coercion to SUP failure in factor<br/>
 <a href="patches/20150126.03.tpd.patch">20150126.03.tpd.patch</a>
 buglist: bug 7299: docker image does not contain GCC<br/>
+<a href="patches/20150129.01.tpd.patch">20150129.01.tpd.patch</a>
+books/bookvol13 add Lamport 21st Century Proofs paper<br/>
  </body>
 </html>
 
-- 
1.7.5.4