equal
deleted
inserted
replaced
93 \begin{isamarkuptext}% |
93 \begin{isamarkuptext}% |
94 Although set syntax in HOL is already close to |
94 Although set syntax in HOL is already close to |
95 standard, we provide a few further improvements: |
95 standard, we provide a few further improvements: |
96 \begin{itemize} |
96 \begin{itemize} |
97 \item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}. |
97 \item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}. |
98 \item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}. |
98 \item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}, where |
|
99 \isa{{\isasymemptyset}} is also input syntax. |
99 \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}}. |
100 \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}}. |
100 \end{itemize}% |
101 \end{itemize}% |
101 \end{isamarkuptext}% |
102 \end{isamarkuptext}% |
102 \isamarkuptrue% |
103 \isamarkuptrue% |
103 % |
104 % |
106 \isamarkuptrue% |
107 \isamarkuptrue% |
107 % |
108 % |
108 \begin{isamarkuptext}% |
109 \begin{isamarkuptext}% |
109 If lists are used heavily, the following notations increase readability: |
110 If lists are used heavily, the following notations increase readability: |
110 \begin{itemize} |
111 \begin{itemize} |
111 \item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}. |
112 \item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}, |
112 Exceptionally, \isa{x{\isasymcdot}xs} is also input syntax. |
113 where \isa{x{\isasymcdot}xs} is also input syntax. |
113 If you prefer more space around the $\cdot$ you have to redefine |
114 If you prefer more space around the $\cdot$ you have to redefine |
114 \verb!\isasymcdot! in \LaTeX: |
115 \verb!\isasymcdot! in \LaTeX: |
115 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
116 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
116 |
117 |
117 \item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}. |
118 \item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}. |