# HG changeset patch
# User wenzelm
# Date 1379777822 -7200
# Node ID 3806bf1d2a333e814896f63cb971ca7ba2bfa2d9
# Parent  ab1ae01b41bc2071ce2095891a62b92d4c3f28b0
more front-matter;

diff -r ab1ae01b41bc -r 3806bf1d2a33 src/Doc/JEdit/document/root.tex
--- 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}