src/HOL/Hoare_Parallel/document/root.bib

commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
the "lfp"/"gfp" bug can be reproduced by looking for a counterexample to
lemma "(A \<union> B)^+ = A^+ \<union> B^+"
Refute incorrectly finds a countermodel for cardinality 1 (the smallest
counterexample requires cardinality 2).

@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}