# HG changeset patch
# User nipkow
# Date 1400224755 -7200
# Node ID a33fe940a557a51772587b2f7cd2c2a6e554b626
# Parent  dc01225a2f773d1e3a48d5d06e88f22e930dd72e
new syntax for card, normalized spacing for #

diff -r dc01225a2f77 -r a33fe940a557 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Thu May 15 16:46:29 2014 +0200
+++ b/src/Doc/Sugar/Sugar.thy	Fri May 16 09:19:15 2014 +0200
@@ -9,9 +9,9 @@
 This document is for those Isabelle users who have mastered
 the art of mixing \LaTeX\ text and Isabelle theories and never want to
 typeset a theorem by hand anymore because they have experienced the
-bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
+bliss of writing \verb!@!\verb!{thm[display,mode=latex_sum] setsum_Suc_diff [no_vars]}!
 and seeing Isabelle typeset it for them:
-@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
+@{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]}
 No typos, no omissions, no sweat.
 If you have not experienced that joy, read Chapter 4, \emph{Presenting
 Theories}, \cite{LNCS2283} first.
@@ -72,6 +72,7 @@
 \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))"}.
+\item @{term"card A"} instead of @{text"card A"}.
 \end{itemize}
 
 
@@ -81,10 +82,6 @@
 \begin{itemize}
 \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\,}}!
-
 \item @{term"length xs"} instead of @{text"length xs"}.
 \item @{term"nth xs n"} instead of @{text"nth xs n"},
       the $n$th element of @{text xs}.
diff -r dc01225a2f77 -r a33fe940a557 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu May 15 16:46:29 2014 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri May 16 09:19:15 2014 +0200
@@ -48,11 +48,15 @@
   "_Collect p P"      <= "{p|xs. P}"
   "_CollectIn p A P"  <= "{p : A. P}"
 
+(* card *)
+notation (latex output)
+  card  ("|_|")
+
 (* LISTS *)
 
 (* Cons *)
 notation (latex)
-  Cons  ("_\<cdot>/_" [66,65] 65)
+  Cons  ("_ \<cdot>/ _" [66,65] 65)
 
 (* length *)
 notation (latex output)