equal
deleted
inserted
replaced
17 \begin{isamarkuptext}% |
17 \begin{isamarkuptext}% |
18 \noindent |
18 \noindent |
19 The infix function \isa{{\isacharbang}} yields the nth element of a list.% |
19 The infix function \isa{{\isacharbang}} yields the nth element of a list.% |
20 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
21 % |
21 % |
22 \isamarkupsubsubsection{Predefined overloading% |
22 \isamarkupsubsubsection{Predefined Overloading% |
23 } |
23 } |
24 % |
24 % |
25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 HOL comes with a number of overloaded constants and corresponding classes. |
26 HOL comes with a number of overloaded constants and corresponding classes. |
27 The most important ones are listed in Table~\ref{tab:overloading}. They are |
27 The most important ones are listed in Table~\ref{tab:overloading}. They are |
45 \isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ |
45 \isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ |
46 \isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ |
46 \isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\ |
47 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & |
47 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & |
48 \isa{LEAST}$~x.~P$ |
48 \isa{LEAST}$~x.~P$ |
49 \end{tabular} |
49 \end{tabular} |
50 \caption{Overloaded constants in HOL} |
50 \caption{Overloaded Constants in HOL} |
51 \label{tab:overloading} |
51 \label{tab:overloading} |
52 \end{center} |
52 \end{center} |
53 \end{table} |
53 \end{table} |
54 |
54 |
55 In addition there is a special input syntax for bounded quantifiers: |
55 In addition there is a special input syntax for bounded quantifiers: |