diff -r 286c1741285c -r e89cfc004f18 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Wed Nov 18 17:37:00 2015 +0000
+++ b/src/Doc/Locales/Examples3.thy	Wed Nov 18 21:18:33 2015 +0100
@@ -223,15 +223,13 @@
 
   \hspace*{1em}@{thm [source] le'.less_le_trans}:
   @{thm [display, indent=4] le'.less_le_trans}
-  While there is infix syntax for the strict operation associated to
+  While there is infix syntax for the strict operation associated with
   @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
-  "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
+  "op \<preceq>"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
   available for the original instance it was declared for.  We may
-  introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
-  with the following declaration:\<close>
+  introduce infix syntax for @{text le'.less} with the following declaration:\<close>
 
-  abbreviation (in order_preserving)
-    less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
+  notation (in order_preserving) le'.less (infixl "\<prec>" 50)
 
 text (in order_preserving) \<open>Now the theorem is displayed nicely as
   @{thm [source]  le'.less_le_trans}:
@@ -306,8 +304,8 @@
 
   context lattice_hom
   begin
-  abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
-  abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
+  notation le'.meet (infixl "\<sqinter>''" 50)
+  notation le'.join (infixl "\<squnion>''" 50)
   end
 
 text \<open>The next example makes radical use of the short hand