--- a/thys/RIPEMD-160-SPARK/document/root.tex
+++ b/thys/RIPEMD-160-SPARK/document/root.tex
@@ -38,12 +38,7 @@
 \maketitle
 
 \begin{abstract}
-  Functional Specification of the cryptographic hash-function RIPEMD-160
-  \cite{ripemd} in Isabelle/HOL \cite{LNCS2283}. Verification of the functional
-  correctness of an implementation in SPARK/ADA \cite{highintegritysoftware}
-  with proofs for the verification conditions generated by the static-analysis
-  toolset of SPARK, translated to Isabelle/HOL with
-  a modified version of Victor-0.8.0\cite{vct}.
+This work presents a verification of an implementation in SPARK/ADA \cite{highintegritysoftware} of the cryptographic hash-function RIPEMD-160. A functional specification of RIPEMD-160 \cite{ripemd} is given in Isabelle/HOL \cite{LNCS2283}. Proofs for the verification conditions generated by the static-analysis toolset of SPARK certify the functional correctness of the implementation. The verification conditions are translated to Isabelle/HOL with a modified version of Victor-0.8.0 \cite{vct}.
 \end{abstract}
 
 \tableofcontents