doc-src/TutorialI/Documents/Documents.thy

   expressions.  This essentially provides a simple mechanism for
   syntactic macros; even heavier transformations may be written in ML
   \cite{isabelle-ref}.
 
   \medskip A typical example of syntax translations is to decorate
-  relational expressions with nice symbolic notation, such as @{text
-  "(x, y) \<in> sim"} versus @{text "x \<approx> y"}.
+  relational expressions (i.e.\ set-membership of tuples) with
+  handsome symbolic notation, such as @{text "(x, y) \<in> sim"} versus
+  @{text "x \<approx> y"}.
 *}
 
 consts
   sim :: "('a \<times> 'a) set"