From 1e3fd58e7177b995e3aa07f6583409584fae026f Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Thu, 10 Oct 2013 14:58:18 +0000
Subject: [PATCH] added reference to Stefan Hallerstede's proof obligation
paper
git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15974 1434b563-b632-4741-aa49-43a3a8374d2e
---
org.rodinp.handbook.feature/latex/rodin-doc.tex | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex
index 74abb53..76371bf 100644
--- a/org.rodinp.handbook.feature/latex/rodin-doc.tex
+++ b/org.rodinp.handbook.feature/latex/rodin-doc.tex
@@ -223,8 +223,13 @@ Those interested in more general guidelines on how to develop and structure form
\subsection{Proofs for the Working Engineer (2008)}
In his dissertation at the ETH Zurich Fahrad Mehta describes how theorem proving
-can be a practical tool for an engineer and presented the ideas that are used
-in building the fundament of Rodin.
+can be a practical tool for software engineers and presents the ideas that are used
+in building Rodin's infrastructure.
+
+\subsection{The Proof Obligation Generator (2005)}
+In this technical report (ETH Zürich) Stefan Hallerstede describes which proof obligations
+(see Section~\ref{generated_proof_obligations}) are generated for a model
+and gives a justification why these are correct.
\section{Conventions}
\label{conventions}
--
GitLab