diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex index 74abb5390e59d691d3c6710f6f5cf91b78158f05..76371bf69564b004bcac8029c7e66e476fe1f390 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}