src/Doc/Locales/Examples3.thy

   sublocale non_negative \<subseteq>
       order_preserving "(\<le>)" "(\<le>)" "\<lambda>i. n * i"
     using non_neg by unfold_locales (rule mult_left_mono)
 
 text \<open>While the proof of the previous interpretation
-  is straightforward from monotonicity lemmas for~@{term "( * )"}, the
+  is straightforward from monotonicity lemmas for~@{term "(*)"}, the
   second proof follows a useful pattern.\<close>
 
   sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i"
   proof (unfold_locales, unfold int_min_eq int_max_eq)
     txt \<open>\normalsize Unfolding the locale predicates \emph{and} the