# HG changeset patch
# User wenzelm
# Date 1694453448 -7200
# Node ID b5f3d1051b131a80b1e4560cc05e5a3d223bc64f
# Parent  71536ae52b16c07b93af6b813a3a115be092cb2c
tuned;

diff -r 71536ae52b16 -r b5f3d1051b13 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Sep 11 15:59:40 2023 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Sep 11 19:30:48 2023 +0200
@@ -1994,7 +1994,7 @@
 
   \<^medskip> The GUI elements of the \<^emph>\<open>Document\<close> panel (\figref{fig:document}), and its
   sub-panels for \<^emph>\<open>Input\<close> and \<^emph>\<open>Output\<close> are described below (from left to
-  right). The screenshot of has two instances of the panel to illustrate both
+  right). The screenshot has two instances of the panel to illustrate both
   \<^emph>\<open>Input\<close> and \<^emph>\<open>Output\<close> simultaneously.
 
     \<^item> The \<^emph>\<open>session selector\<close> tells, which session should be the basis of the