diff -r 4872b10c8747 -r be4fca364690 doc-src/isac/CTP-userinterfaces.tex
--- a/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 08:03:23 2011 +0100
+++ b/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 12:34:29 2011 +0100
@@ -20,7 +20,9 @@
 \begin{document}
 \maketitle
 \abstract{
-TODO}
+
+
+}
 
 \section{Introduction}\label{intro}
 Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations.