# HG changeset patch
# User oheimb
# Date 1089637530 -7200
# Node ID eb2469e495cd601f35f63034e66f216f0e627824
# Parent  19b3b0382303bdc057a691008bac7d90546815cf
corrected bibtex entry

diff -r 19b3b0382303 -r eb2469e495cd src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Mon Jul 12 12:11:46 2004 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy	Mon Jul 12 15:05:30 2004 +0200
@@ -4,17 +4,20 @@
 
 Formalization of section 4 of
 
-@inproceedings{Broy95-SRBLO,
-        author = {Manfred Broy},
-        title = {Specification and ReFinement of a Buffer of Length One},
-        booktitle = {Working Material of Marktoberdorf Summer School},
-        year = {1994},
-        publisher = {},
-        editor = {},
-        note = {\url{http://www4.in.tum.de/papers/broy_mod94.html}}
+@inproceedings {broy_mod94,
+    author = {Manfred Broy},
+    title = {{Specification and Refinement of a Buffer of Length One}},
+    booktitle = {Deductive Program Design},
+    year = {1994},
+    editor = {Manfred Broy},
+    volume = {152},
+    series = {ASI Series, Series F: Computer and System Sciences},
+    pages = {273 -- 304},
+    publisher = {Springer}
 }
 
 Slides available from http://isabelle.in.tum.de/HOLCF/1-Buffer.ps.gz
+
 *)
 
 Buffer = FOCUS +