--- 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\,}}!
--- 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\,}}!
--- 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)