From 5569fc139e81c8d3f59eb65d7ead53e863b954bf Mon Sep 17 00:00:00 2001
From: Tim Daly
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/axiomwebsite/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 =
\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 2024, 1999, pp 17581777
\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/enus/um/people/lamport/tla/errata1.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/enus/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/axiomwebsite/patches.html 20150129.01.tpd.patch
+20150129 tpd books/bookvol13 add Lamport 21st Century Proofs paper
20150126 tpd src/axiomwebsite/patches.html 20150126.03.tpd.patch
20150126 tpd buglist: bug 7299: docker image does not contain GCC
20150126 wxh src/axiomwebsite/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/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 7e834df..08a952f 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 4980,6 +4980,8 @@ books/bookvol10.3 fixed bug 7297: Extraneous "#\" characters
bookvol10.4 MLIFT bug 7298: coercion to SUP failure in factor
20150126.03.tpd.patch
buglist: bug 7299: docker image does not contain GCC
+20150129.01.tpd.patch
+books/bookvol13 add Lamport 21st Century Proofs paper

1.7.5.4