--- a/src/HOL/Data_Structures/document/root.bib Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.bib Tue Sep 22 08:38:25 2015 +0200
@@ -1,20 +1,12 @@
-@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
-@string{MIT="MIT Press"}
-@string{Springer="Springer-Verlag"}
-
-@book{Nielson,author={Hanne Riis Nielson and Flemming Nielson},
-title={Semantics with Applications},publisher={Wiley},year=1992}
+@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
+journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
-@book{Winskel,author={Glynn Winskel},
-title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
+@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
+note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}
-@inproceedings{Nipkow,author={Tobias Nipkow},
-title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
-booktitle=
-{Foundations of Software Technology and Theoretical Computer Science},
-editor={V. Chandru and V. Vinay},
-publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
+@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. A Proof Assistant Approach},publisher=Springer,
-note={To appear}}
+title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
+year=2014}