--- a/src/Doc/JEdit/JEdit.thy Thu May 21 14:03:17 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri May 22 15:10:35 2015 +0200
@@ -315,7 +315,7 @@
in mind that this extra variance of GUI functionality is unlikely to
work in arbitrary combinations. The platform-independent
\emph{Nimbus} and \emph{Metal} should always work. The historic
- \emph{CDE/Motif} is better ignore altogether.
+ \emph{CDE/Motif} should be ignored.
After changing the look-and-feel in \emph{Global Options~/
Appearance}, it is advisable to restart Isabelle/jEdit in order to