# HG changeset patch
# User boehmes
# Date 1257428497 -3600
# Node ID cba964797872533dbea59148a36ea0e28fe8c26b
# Parent  c8bc8dc5869ffe574f00835a06f8e39130ec9610
added references to HOL-Boogie papers

diff -r c8bc8dc5869f -r cba964797872 src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Wed Nov 04 17:17:30 2009 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Thu Nov 05 14:41:37 2009 +0100
@@ -13,6 +13,22 @@
   ("Tools/boogie_split.ML")
 begin
 
+text {*
+HOL-Boogie and its applications are described in:
+\begin{itemize}
+
+\item Sascha B"ohme, K. Rustan M. Leino, and Burkhart Wolff.
+HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier.
+Theorem Proving in Higher Order Logics, 2008.
+
+\item Sascha B"ohme, Micha{\l} Moskal, Wolfram Schulte, and Burkhart Wolff.
+HOL-Boogie --- An Interactive Prover-Backend for the Verifying C Compiler.
+Journal of Automated Reasoning, 2009.
+
+\end{itemize}
+*}
+
+
 section {* Built-in types and functions of Boogie *}
 
 subsection {* Labels *}