src/Doc/Locales/Examples3.thy

--- a/src/Doc/Locales/Examples3.thy	Tue Jul 05 11:47:49 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy	Tue Jul 05 17:52:08 2016 +0200
@@ -408,7 +408,7 @@
     assumes non_neg: "0 \<le> n"
 
 text \<open>It is again convenient to make the interpretation in an
-  incremental fashion, first for order preserving maps, the for
+  incremental fashion, first for order preserving maps, then for
   lattice endomorphisms.\<close>
 
   sublocale non_negative \<subseteq>