diff -r c185d9f262d1 -r f49671358ddb doc-src/isac/CTP-userinterfaces.tex
--- a/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 13:50:02 2011 +0100
+++ b/doc-src/isac/CTP-userinterfaces.tex	Tue Jan 11 14:05:20 2011 +0100
@@ -20,7 +20,11 @@
 \begin{document}
 \maketitle
 \abstract{
-TODO}
+This paper accompanies a pre-study on a sub-project planned within the \sisac-project. The goal of this sub-project is to extend ther userinterface of the theorem prover Isabelle such, that Structured Derivations according to R.J.Back are interactively processed. The sub-project is one step towards using the upcoming Isabelle/Isar/Scala layer for /sisac.
+
+The paper comprises three parts: (1) Ample space is given to background information about the state of the art in user interfaces for theorem provers and about the upcoming requirements for future developments. (2) focuses the strategy of Isabelle, the motivations and first decision. (3) provides a protocol of preparatory work for the sub-project.
+
+By the way, this paper shall serve as an entry point for students interested in joining the \sisac-team.}
 
 \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.
@@ -114,7 +118,7 @@
 
 %(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
 \subsubsection{Proof General for Isabelle}
-Proof General is a generic front-end for proof assistants \cite{aspinall}, based on the text editor Emacs.
+Proof General is a generic front-end for proof assistants \cite{Aspinall:2007:FIP:1420412.1420429}, based on the text editor Emacs.
 It has been developed at the University of Edinburgh with contributions from other sites.
 Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO.
 It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. 
@@ -131,7 +135,7 @@
 \includegraphics[scale=0.25]{fig/pgisabelle}
 \caption{Proof General for Isabelle}%
 \end{figure}
-\newpage
+
 \subsubsection{Isabelle/Jedit}
 jEdit is a text editor for programmers, written in Java.
 Compared to fully-featured IDEs, such as Eclipse or Netbeans, jEdit is much