\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}
