--- a/doc-src/TutorialI/Documents/Documents.thy Tue Jan 08 17:43:21 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Tue Jan 08 17:51:56 2002 +0100
@@ -252,8 +252,9 @@
\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
--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 17:43:21 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 17:51:56 2002 +0100
@@ -249,7 +249,9 @@
\cite{isabelle-ref}.
\medskip A typical example of syntax translations is to decorate
- relational expressions with nice symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
+ relational expressions (i.e.\ set-membership of tuples) with
+ handsome symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus
+ \isa{x\ {\isasymapprox}\ y}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline