diff -r dacc380ab327 -r e7df93d4d9b8 src/Doc/Locales/Examples.thy
--- a/src/Doc/Locales/Examples.thy	Thu Aug 25 20:08:40 2016 +0200
+++ b/src/Doc/Locales/Examples.thy	Thu Aug 25 20:08:41 2016 +0200
@@ -320,7 +320,8 @@
 
 text \<open>These assumptions refer to the predicates for infimum
   and supremum defined for @{text partial_order} in the previous
-  section.  We now introduce the notions of meet and join.\<close>
+  section.  We now introduce the notions of meet and join,
+  together with an example theorem.\<close>
 
   definition
     meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)"
@@ -345,8 +346,7 @@
       by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y i\<close>])
   qed
 
-  lemma %invisible meet_left [intro?]:
-    "x \<sqinter> y \<sqsubseteq> x"
+  lemma meet_left(*<*)[intro?](*>*): "x \<sqinter> y \<sqsubseteq> x"
     by (rule is_inf_lower) (rule is_inf_meet)
 
   lemma %invisible meet_right [intro?]:
@@ -568,8 +568,7 @@
 
 text \<open>Locales for total orders and distributive lattices follow to
   establish a sufficiently rich landscape of locales for
-  further examples in this tutorial.  Each comes with an example
-  theorem.\<close>
+  further examples in this tutorial.\<close>
 
   locale total_order = partial_order +
     assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"