tuned;
authorwenzelm
Tue, 13 Nov 2018 11:30:44 +0100
changeset 69298 06fda16e50fb
parent 69297 36d711008292
child 69299 72a9860f8602
tuned;
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,