From fff949ebb112ce3a50b581931f24de11e19bcf2a Mon Sep 17 00:00:00 2001
From: Tim Daly <daly@axiom-developer.org>
Date: Mon, 30 Nov 2015 21:32:47 -0500
Subject: [PATCH] books/bookvolbib add Kreb15

Goal: Proving Axiom correct

@phdthesis{Kreb15,
  author = "Krebbers, Robbert Jan",
  title = "The C standard formalized in Coq",
  school = "Radboud University",
  year = "2015",
  file = "Kreb15.pdf",
  url = "http://robbertkrebbers.nl/thesis.html"

}
---
 books/bookvolbib.pamphlet      |   14 ++++++++++++++
 changelog                      |    2 ++
 patch                          |   15 ++++++++++++---
 src/axiom-website/patches.html |    2 ++
 4 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index a9ca494..43c4b9b 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2613,6 +2613,20 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
 
 \end{chunk}
 
+\index{Krebbers, Robbert Jan}
+\begin{chunk}{axiom.bib}
+@phdthesis{Kreb15,
+  author = "Krebbers, Robbert Jan",
+  title = "The C standard formalized in Coq",
+  school = "Radboud University",
+  year = "2015",
+  file = "Kreb15.pdf",
+  url = "http://robbertkrebbers.nl/thesis.html"
+
+}
+
+\end{chunk}
+
 \index{Mahboubi, Assia}
 \begin{chunk}{axiom.bib}
 @article{Mahb06,
diff --git a/changelog b/changelog
index a89cfd4..64be411 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20151130 tpd src/axiom-website/patches.html 20151130.02.tpd.patch
+20151130 tpd books/bookvolbib add Kreb15
 20151130 tpd src/axiom-website/patches.html 20151130.01.tpd.patch
 20151130 tpd src/input/Makefile add combinatorics.input
 20151130 axa src/input/combinatorics.input add work by Alasdair McAndrew
diff --git a/patch b/patch
index 65a1160..be2e9a4 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,14 @@
-src/input/combinatorics.input add work by Alasdair McAndrew
+books/bookvolbib add Kreb15
 
-Goal: example algebra
+Goal: Proving Axiom correct
+
+@phdthesis{Kreb15,
+  author = "Krebbers, Robbert Jan",
+  title = "The C standard formalized in Coq",
+  school = "Radboud University",
+  year = "2015",
+  file = "Kreb15.pdf",
+  url = "http://robbertkrebbers.nl/thesis.html"
+
+}
 
-Add combinatorics example by Alasdair McAndrew
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 03f4459..bbff863 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5140,6 +5140,8 @@ books/bookvolbib add Engl13<br/>
 books/bookvolbib add Engl15<br/>
 <a href="patches/20151130.01.tpd.patch">20151130.01.tpd.patch</a>
 src/input/combinatorics.input add work by Alasdair McAndrew<br/>
+<a href="patches/20151130.02.tpd.patch">20151130.02.tpd.patch</a>
+books/bookvolbib add Kreb15<br/>
  </body>
 </html>
 
-- 
1.7.5.4