--- a/src/HOL/Data_Structures/document/root.bib Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.bib Tue Sep 22 14:31:22 2015 +0200
@@ -6,7 +6,3 @@
@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}
-
-@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
-title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
-year=2014}
--- a/src/HOL/IMP/document/root.bib Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/IMP/document/root.bib Tue Sep 22 14:31:22 2015 +0200
@@ -15,6 +15,6 @@
editor={V. Chandru and V. Vinay},
publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
-@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
-title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
-note={To appear}}
+@book{NipkowK2014,author={Tobias Nipkow and Gerwin Klein},
+title={Concrete Semantics with Isabelle/HOL},publisher="Springer",
+year=2014,note={\url{http://concrete-semantics.org}}}
--- a/src/HOL/IMP/document/root.tex Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/IMP/document/root.tex Tue Sep 22 14:31:22 2015 +0200
@@ -23,6 +23,10 @@
\author{Tobias Nipkow \& Gerwin Klein}
\maketitle
+\begin{abstract}
+This document presents formalizations of the semantics of a simple imperative programming language together with a number of applications: a compiler, type systems, various program analyses and abstract interpreters. These theories form the basis of the book \emph{Concrete Semantics with Isabelle/HOL} by Nipkow and Klein \cite{NipkowK2014}.
+\end{abstract}
+
\setcounter{tocdepth}{2}
\tableofcontents
\newpage
--- a/src/HOL/Library/RBT_Impl.thy Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 22 14:31:22 2015 +0200
@@ -331,6 +331,8 @@
subsection \<open>Insertion\<close>
+text \<open>The function definitions are based on the book by Okasaki.\<close>
+
fun (* slow, due to massive case splitting *)
balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
@@ -554,6 +556,9 @@
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto
+text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
+at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
+
fun
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where