new syntax for card, normalized spacing for #
authornipkow
Fri May 16 09:19:15 2014 +0200 (2014-05-16)
changeset 56977a33fe940a557
parent 56976 dc01225a2f77
child 56978 0c1b4987e6b2
new syntax for card, normalized spacing for #
src/Doc/Sugar/Sugar.thy
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/src/Doc/Sugar/Sugar.thy	Thu May 15 16:46:29 2014 +0200
     1.2 +++ b/src/Doc/Sugar/Sugar.thy	Fri May 16 09:19:15 2014 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  This document is for those Isabelle users who have mastered
     1.5  the art of mixing \LaTeX\ text and Isabelle theories and never want to
     1.6  typeset a theorem by hand anymore because they have experienced the
     1.7 -bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
     1.8 +bliss of writing \verb!@!\verb!{thm[display,mode=latex_sum] setsum_Suc_diff [no_vars]}!
     1.9  and seeing Isabelle typeset it for them:
    1.10 -@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
    1.11 +@{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]}
    1.12  No typos, no omissions, no sweat.
    1.13  If you have not experienced that joy, read Chapter 4, \emph{Presenting
    1.14  Theories}, \cite{LNCS2283} first.
    1.15 @@ -72,6 +72,7 @@
    1.16  \item @{term"{}"} instead of @{text"{}"}, where
    1.17   @{term"{}"} is also input syntax.
    1.18  \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
    1.19 +\item @{term"card A"} instead of @{text"card A"}.
    1.20  \end{itemize}
    1.21  
    1.22  
    1.23 @@ -81,10 +82,6 @@
    1.24  \begin{itemize}
    1.25  \item @{term"x # xs"} instead of @{text"x # xs"},
    1.26        where @{term"x # xs"} is also input syntax.
    1.27 -If you prefer more space around the $\cdot$ you have to redefine
    1.28 -\verb!\isasymcdot! in \LaTeX:
    1.29 -\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
    1.30 -
    1.31  \item @{term"length xs"} instead of @{text"length xs"}.
    1.32  \item @{term"nth xs n"} instead of @{text"nth xs n"},
    1.33        the $n$th element of @{text xs}.
     2.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu May 15 16:46:29 2014 +0200
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri May 16 09:19:15 2014 +0200
     2.3 @@ -48,11 +48,15 @@
     2.4    "_Collect p P"      <= "{p|xs. P}"
     2.5    "_CollectIn p A P"  <= "{p : A. P}"
     2.6  
     2.7 +(* card *)
     2.8 +notation (latex output)
     2.9 +  card  ("|_|")
    2.10 +
    2.11  (* LISTS *)
    2.12  
    2.13  (* Cons *)
    2.14  notation (latex)
    2.15 -  Cons  ("_\<cdot>/_" [66,65] 65)
    2.16 +  Cons  ("_ \<cdot>/ _" [66,65] 65)
    2.17  
    2.18  (* length *)
    2.19  notation (latex output)