From ffcb776d1ddf80cf96810f855d7230ee790eddf1 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 8 May 2015 05:13:31 0400
Subject: [PATCH] books/bookvolbib add Robe15 reference
@misc{Robe15,
author = "Roberts, Siobhan",
title = "In Mathematics, Mistakes Aren't What They Used To Be",
year = 2015,
url = "http://nautil.us/issue/24/error/Inmathematicsmistakesarentwhattheyusedtobe"

books/bookvolbib.pamphlet  53 ++++++++
changelog  2 +
patch  9 +++++
src/axiomwebsite/patches.html  2 +
4 files changed, 22 insertions(+), 44 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 1139664..d687618 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 2801,48 +2801,6 @@ FME'99, Toulouse, France, Sept 2024, 1999, pp 17581777
\end{chunk}
\index{Kamareddine, Fairouz}
\index{Wells, Joe}
\index{Zengler, Christoph}
\index{Barendregt, Henk}
\begin{chunk}{axiom.bib}
@misc{Kama15,
 author = "Kamareddine, Fairouz and Wells, Joe and Zengler, Christoph and
 Barendregt, Henk",
 title = "Computerising Mathematical Text",
 url =
"http://repository.ubn.ru.nl/bitstream/handle/2066/134655/134655.pdf?sequence=1",
 paper = "Kama15.pdf",
 abstract =
 "Mathematical texts can be computerised in many ways that capture
 differing amounts of the mathematical meaning. At one end, there is
 document imag ing, which captures the arrangement of black marks on
 paper, while at the other end there are proof assistants (e.g., Mizar,
 Isabelle, Coq, etc.), which capture the full mathematical meaning and
 have proofs expressed in a formal foundation of mathematics. In
 between, there are computer typesetting systems (e.g., LATEX and
 Presentation MathML) and semantically oriented systems (e.g., Content
 MathML, OpenMath, OMDoc, etc.). In this paper we advocate a style of
 computerisation of mathematical texts which is flexible enough to
 connect the different approaches to computerisation, which allows
 various degrees of formalisation, and which is compatible with
 different logical frameworks (e.g., set theory, category theory, type
 theory, etc.) and proof systems. The basic idea is to allow a
 manmachine collaboration which weaves human input with machine
 computation at every step in the way. We propose that the huge step
 from informal mathematics to fully formalised mathematics be divided
 into smaller steps, each of which is a fully developed method in which
 human input is minimal. Let us consider the following two questions:
 \begin{enumerate}
 \item What is the relationship between the logical foundations of
 mathematical reasoning and the actual practice of mathematicians?
 \item In what ways can computers support the development and
 communication of mathematical knowledge?
 \end{enumerate}"
}

\end{chunk}

\index{Lamport, Leslie}
\begin{chunk}{axiom.bib}
@book{Lamp02,
@@ 3070,6 +3028,17 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Roberts, Siobhan}
+\begin{chunk}{axiom.bib}
+@misc{Robe15,
+ author = "Roberts, Siobhan",
+ title = "In Mathematics, Mistakes Aren't What They Used To Be",
+ year = 2015,
+ url = "http://nautil.us/issue/24/error/Inmathematicsmistakesarentwhattheyusedtobe"
+}
+
+\end{chunk}
+
\section{Interval Arithmetic} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Boehm, HansJ.}
diff git a/changelog b/changelog
index 2db984b..c225ca1 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20150508 tpd src/axiomwebsite/patches.html 20150508.01.tpd.patch
+20150508 tpd books/bookvolbib add Robe15 reference
20150505 tpd src/axiomwebsite/patches.html 20150505.02.tpd.patch
20150515 tpd books/bookvol13 add Kama15 reference
20150505 tpd src/axiomwebsite/patches.html 20150505.01.tpd.patch
diff git a/patch b