# HG changeset patch
# User nipkow
# Date 1442925082 -7200
# Node ID 1a690dce8cfce5dfdc538ab9bfdec2187cded560
# Parent  759b5299a9f2c271168cf353b34dd1726bc9525f
tuned references

diff -r 759b5299a9f2 -r 1a690dce8cfc src/HOL/Data_Structures/document/root.bib
--- 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}
diff -r 759b5299a9f2 -r 1a690dce8cfc src/HOL/IMP/document/root.bib
--- 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}}}
diff -r 759b5299a9f2 -r 1a690dce8cfc src/HOL/IMP/document/root.tex
--- 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
diff -r 759b5299a9f2 -r 1a690dce8cfc src/HOL/Library/RBT_Impl.thy
--- 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