author | blanchet |
Tue, 05 Jul 2016 17:52:08 +0200 | |
changeset 63390 | c27edca2d827 |
parent 63389 | 5d8607370faf |
child 63391 | 6840e808fe44 |
--- 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>