# HG changeset patch
# User nipkow
# Date 1144661655 -7200
# Node ID 259e2bbba43c193f621b45376f7c63d51a3fc267
# Parent  17382f02079e0444d100ae377e22d924f889cc75
added references

diff -r 17382f02079e -r 259e2bbba43c src/HOL/HoareParallel/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HoareParallel/document/root.bib	Mon Apr 10 11:34:15 2006 +0200
@@ -0,0 +1,28 @@
+@inproceedings{NipkowP-FASE99,author={Tobias Nipkow and Prensa Nieto, Leonor},
+title={{Owicki/Gries} in {Isabelle/HOL}},
+booktitle={Fundamental Approaches to Software Engineering (FASE'99)},
+editor={J.-P. Finance},publisher="Springer",series="LNCS",volume=1577,
+pages={188--203},year=1999}
+
+@InProceedings{PrenEsp00,
+  author =    {Prensa Nieto, Leonor and Javier Esparza}, 
+  title =     {Verifying Single and Multi-mutator Garbage Collectors
+                with {Owicki/Gries} in {Isabelle/HOL}},
+  booktitle = {Mathematical Foundations of Computer Science (MFCS 2000)},
+  editor =    {M. Nielsen and B. Rovan},
+  publisher = {Springer-Verlag},
+  series =    {LNCS},
+  volume =    1893, 
+  pages =     {619--628},
+  year =      2000
+}
+
+@PhdThesis{Prensa-PhD,author={Leonor Prensa Nieto},
+title={Verification of Parallel Programs with the Owicki-Gries and
+Rely-Guarantee Methods in Isabelle/HOL},
+school={Technische Universit{\"a}t M{\"u}nchen},year=2002}
+
+@inproceedings{Prensa-ESOP03,author={Prensa Nieto, Leonor},
+title={The {Rely-Guarantee} Method in {Isabelle/HOL}},
+booktitle={European Symposium on Programming (ESOP'03)},editor={P. Degano},
+publisher=Springer,series=LNCS,volume=2618,pages={348--362},year=2003}
diff -r 17382f02079e -r 259e2bbba43c src/HOL/HoareParallel/document/root.tex
--- a/src/HOL/HoareParallel/document/root.tex	Mon Apr 10 11:33:36 2006 +0200
+++ b/src/HOL/HoareParallel/document/root.tex	Mon Apr 10 11:34:15 2006 +0200
@@ -36,6 +36,9 @@
   verification of two garbage-collection algorithms, the second one
   parameterized in the number of mutators.
 
+For excellent descriptions of this work see
+\cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}.
+
 \end{abstract}
 
 \pagestyle{plain}
@@ -53,7 +56,7 @@
 \parindent 0pt\parskip 0.5ex
 \input{session}
 
-%\bibliographystyle{plain}
-%\bibliography{root}
+\bibliographystyle{plain}
+\bibliography{root}
 
 \end{document}