--- a/src/Doc/JEdit/document/root.tex Sat Sep 21 17:20:08 2013 +0200
+++ b/src/Doc/JEdit/document/root.tex Sat Sep 21 17:37:02 2013 +0200
@@ -26,6 +26,31 @@
\maketitle
+\begin{abstract}
+ Isabelle/jEdit is a fully-featured Prover IDE, based on Isabelle/Scala and
+ the jEdit text editor. This document provides an overview of general
+ principles and its main IDE functionality.
+\end{abstract}
+
+\vspace*{2.5cm}
+
+\begin{quote}
+ {\small\em Isabelle's user interface is no advance over LCF's, which is
+ widely condemned as ``user-unfriendly'': hard to use, bewildering to
+ beginners. Hence the interest in proof editors, where a proof can be
+ constructed and modified rule-by-rule using windows, mouse, and menus. But
+ Edinburgh LCF was invented because real proofs require millions of
+ inferences. Sophisticated tools --- rules, tactics and tacticals, the
+ language ML, the logics themselves --- are hard to learn, yet they are
+ essential. We may demand a mouse, but we need better education and
+ training.}
+
+ Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
+\end{quote}
+
+
+\vspace*{2.5cm}
+
\subsubsection*{Acknowledgements}