tuned references
authornipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 612251a690dce8cfc
parent 61224 759b5299a9f2
child 61226 af7bed1360f3
child 61229 0b9c45c4af29
tuned references
src/HOL/Data_Structures/document/root.bib
src/HOL/IMP/document/root.bib
src/HOL/IMP/document/root.tex
src/HOL/Library/RBT_Impl.thy
     1.1 --- a/src/HOL/Data_Structures/document/root.bib	Tue Sep 22 08:38:25 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/document/root.bib	Tue Sep 22 14:31:22 2015 +0200
     1.3 @@ -6,7 +6,3 @@
     1.4  
     1.5  @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
     1.6  publisher="Cambridge University Press",year=1998}
     1.7 -
     1.8 -@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
     1.9 -title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
    1.10 -year=2014}
     2.1 --- a/src/HOL/IMP/document/root.bib	Tue Sep 22 08:38:25 2015 +0200
     2.2 +++ b/src/HOL/IMP/document/root.bib	Tue Sep 22 14:31:22 2015 +0200
     2.3 @@ -15,6 +15,6 @@
     2.4  editor={V. Chandru and V. Vinay},
     2.5  publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
     2.6  
     2.7 -@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
     2.8 -title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
     2.9 -note={To appear}}
    2.10 +@book{NipkowK2014,author={Tobias Nipkow and Gerwin Klein},
    2.11 +title={Concrete Semantics with Isabelle/HOL},publisher="Springer",
    2.12 +year=2014,note={\url{http://concrete-semantics.org}}}
     3.1 --- a/src/HOL/IMP/document/root.tex	Tue Sep 22 08:38:25 2015 +0200
     3.2 +++ b/src/HOL/IMP/document/root.tex	Tue Sep 22 14:31:22 2015 +0200
     3.3 @@ -23,6 +23,10 @@
     3.4  \author{Tobias Nipkow \& Gerwin Klein}
     3.5  \maketitle
     3.6  
     3.7 +\begin{abstract}
     3.8 +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}.
     3.9 +\end{abstract}
    3.10 +
    3.11  \setcounter{tocdepth}{2}
    3.12  \tableofcontents
    3.13  \newpage
     4.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 22 08:38:25 2015 +0200
     4.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 22 14:31:22 2015 +0200
     4.3 @@ -331,6 +331,8 @@
     4.4  
     4.5  subsection \<open>Insertion\<close>
     4.6  
     4.7 +text \<open>The function definitions are based on the book by Okasaki.\<close>
     4.8 +
     4.9  fun (* slow, due to massive case splitting *)
    4.10    balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    4.11  where
    4.12 @@ -554,6 +556,9 @@
    4.13  lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
    4.14  by (cases t rule: rbt_cases) auto
    4.15  
    4.16 +text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
    4.17 +at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
    4.18 +
    4.19  fun
    4.20    balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    4.21  where