diff -r d27f9b4e027d -r b5ce7100ddc8 src/Doc/Prog_Prove/document/root.bib
--- a/src/Doc/Prog_Prove/document/root.bib	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Doc/Prog_Prove/document/root.bib	Mon Apr 03 17:39:08 2017 +0200
@@ -1,6 +1,12 @@
 @string{CUP="Cambridge University Press"}
 @string{LNCS="Lect.\ Notes in Comp.\ Sci."}
-@string{Springer="Springer-Verlag"}
+@string{Springer="Springer"}
+
+@InProceedings{BauerW-TPHOLs01,author={Gertrud Bauer and Markus Wenzel},
+title={Calculational Reasoning Revisited --- An {Isabelle/Isar} Experience},
+booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
+editor={R. Boulton and P. Jackson},
+year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
 
 @book{HuthRyan,author="Michael Huth and Mark Ryan",
 title={Logic in Computer Science},publisher=CUP,year=2004}