# HG changeset patch
# User nipkow
# Date 1217270947 -7200
# Node ID 397de75836a10672894d1e3c43f589a48c1d8b32
# Parent  224a18d1a3acd94632c45a735cf58cdd7bfbc8a8
*** empty log message ***

diff -r 224a18d1a3ac -r 397de75836a1 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sun Jul 27 20:08:16 2008 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Jul 28 20:49:07 2008 +0200
@@ -71,7 +71,8 @@
 standard, we provide a few further improvements:
 \begin{itemize}
 \item @{term"{x. P}"} instead of @{text"{x. P}"}.
-\item @{term"{}"} instead of @{text"{}"}.
+\item @{term"{}"} instead of @{text"{}"}, where
+ @{term"{}"} is also input syntax.
 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
 \end{itemize}
 *}
@@ -80,8 +81,8 @@
 
 text{* If lists are used heavily, the following notations increase readability:
 \begin{itemize}
-\item @{term"x # xs"} instead of @{text"x # xs"}.
-      Exceptionally, @{term"x # xs"} is also input syntax.
+\item @{term"x # xs"} instead of @{text"x # xs"},
+      where @{term"x # xs"} is also input syntax.
 If you prefer more space around the $\cdot$ you have to redefine
 \verb!\isasymcdot! in \LaTeX:
 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
diff -r 224a18d1a3ac -r 397de75836a1 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sun Jul 27 20:08:16 2008 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Mon Jul 28 20:49:07 2008 +0200
@@ -95,7 +95,8 @@
 standard, we provide a few further improvements:
 \begin{itemize}
 \item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}.
-\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}.
+\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}, where
+ \isa{{\isasymemptyset}} is also input syntax.
 \item \isa{{\isacharbraceleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharbraceright}\ {\isasymunion}\ M} instead of \isa{insert\ a\ {\isacharparenleft}insert\ b\ {\isacharparenleft}insert\ c\ M{\isacharparenright}{\isacharparenright}}.
 \end{itemize}%
 \end{isamarkuptext}%
@@ -108,8 +109,8 @@
 \begin{isamarkuptext}%
 If lists are used heavily, the following notations increase readability:
 \begin{itemize}
-\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}.
-      Exceptionally, \isa{x{\isasymcdot}xs} is also input syntax.
+\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs},
+      where \isa{x{\isasymcdot}xs} is also input syntax.
 If you prefer more space around the $\cdot$ you have to redefine
 \verb!\isasymcdot! in \LaTeX:
 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
diff -r 224a18d1a3ac -r 397de75836a1 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Sun Jul 27 20:08:16 2008 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon Jul 28 20:49:07 2008 +0200
@@ -30,17 +30,15 @@
 (* SETS *)
 
 (* empty set *)
-syntax (latex output)
-  "_emptyset" :: "'a set"              ("\<emptyset>")
-translations
-  "_emptyset"      <= "{}"
+notation (latex)
+  "{}" ("\<emptyset>")
 
 (* insert *)
 translations 
   "{x} \<union> A" <= "insert x A"
   "{x,y}" <= "{x} \<union> {y}"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
-  "{x}" <= "{x} \<union> _emptyset"
+  "{x}" <= "{x} \<union> \<emptyset>"
 
 (* set comprehension *)
 syntax (latex output)