69 |
69 |
70 text{* Although set syntax in HOL is already close to |
70 text{* Although set syntax in HOL is already close to |
71 standard, we provide a few further improvements: |
71 standard, we provide a few further improvements: |
72 \begin{itemize} |
72 \begin{itemize} |
73 \item @{term"{x. P}"} instead of @{text"{x. P}"}. |
73 \item @{term"{x. P}"} instead of @{text"{x. P}"}. |
74 \item @{term"{}"} instead of @{text"{}"}. |
74 \item @{term"{}"} instead of @{text"{}"}, where |
|
75 @{term"{}"} is also input syntax. |
75 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
76 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
76 \end{itemize} |
77 \end{itemize} |
77 *} |
78 *} |
78 |
79 |
79 subsection{* Lists *} |
80 subsection{* Lists *} |
80 |
81 |
81 text{* If lists are used heavily, the following notations increase readability: |
82 text{* If lists are used heavily, the following notations increase readability: |
82 \begin{itemize} |
83 \begin{itemize} |
83 \item @{term"x # xs"} instead of @{text"x # xs"}. |
84 \item @{term"x # xs"} instead of @{text"x # xs"}, |
84 Exceptionally, @{term"x # xs"} is also input syntax. |
85 where @{term"x # xs"} is also input syntax. |
85 If you prefer more space around the $\cdot$ you have to redefine |
86 If you prefer more space around the $\cdot$ you have to redefine |
86 \verb!\isasymcdot! in \LaTeX: |
87 \verb!\isasymcdot! in \LaTeX: |
87 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
88 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
88 |
89 |
89 \item @{term"length xs"} instead of @{text"length xs"}. |
90 \item @{term"length xs"} instead of @{text"length xs"}. |