# HG changeset patch
# User wenzelm
# Date 1010508716 -3600
# Node ID 90568836340a326f60149c7ff5ed4f7b45c83a85
# Parent  f85386e8acdf7a9fa657fa87ac4b680e98126df3
tuned;

diff -r f85386e8acdf -r 90568836340a doc-src/TutorialI/Documents/Documents.thy
--- 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
diff -r f85386e8acdf -r 90568836340a doc-src/TutorialI/Documents/document/Documents.tex
--- 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