# HG changeset patch
# User blanchet
# Date 1467733928 -7200
# Node ID c27edca2d8279050c8bf73e302253b556119521a
# Parent  5d8607370faf2a8b214436305578e3e76b5a4c8b
typo (reported by Anders Schlichtkrull)

diff -r 5d8607370faf -r c27edca2d827 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>