# HG changeset patch
# User wenzelm
# Date 1542105044 -3600
# Node ID 06fda16e50fbb65b8670199f563ea6ff5cc3359e
# Parent  36d7110082929a9f4477416f1c68454cb8a4530a
tuned;

diff -r 36d711008292 -r 06fda16e50fb src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Mon Nov 12 16:07:32 2018 +0100
+++ b/src/Doc/Implementation/Prelim.thy	Tue Nov 13 11:30:44 2018 +0100
@@ -277,7 +277,7 @@
   \<^medskip>
 
   The \<open>empty\<close> value acts as initial default for \<^emph>\<open>any\<close> theory that does not
-  declare actual data content; \<open>extend\<close> is acts like a unitary version of
+  declare actual data content; \<open>extend\<close> acts like a unitary version of
   \<open>merge\<close>.
 
   Implementing \<open>merge\<close> can be tricky. The general idea is that \<open>merge (data\<^sub>1,