src/Doc/Implementation/Prelim.thy

   \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & join on import \\
   \end{tabular}
   \<^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,
   data\<^sub>2)\<close> inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet
   present, while keeping the general order of things. The @{ML Library.merge}