equal
deleted
inserted
replaced
39 HOL comes with a number of overloaded constants and corresponding classes. |
39 HOL comes with a number of overloaded constants and corresponding classes. |
40 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
40 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
41 defined on all numeric types and sometimes on other types as well, for example |
41 defined on all numeric types and sometimes on other types as well, for example |
42 $-$ and \isa{{\isasymle}} on sets. |
42 $-$ and \isa{{\isasymle}} on sets. |
43 |
43 |
44 In addition there is a special input syntax for bounded quantifiers: |
44 In addition there is a special syntax for bounded quantifiers: |
45 \begin{center} |
45 \begin{center} |
46 \begin{tabular}{lcl} |
46 \begin{tabular}{lcl} |
47 \isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\ |
47 \isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\ |
48 \isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x} |
48 \isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}} |
49 \end{tabular} |
49 \end{tabular} |
50 \end{center} |
50 \end{center} |
51 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}. |
51 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.% |
52 The form on the left is translated into the one on the right upon input. |
|
53 For technical reasons, it is not translated back upon output.% |
|
54 \end{isamarkuptext}% |
52 \end{isamarkuptext}% |
55 \isamarkuptrue% |
53 \isamarkuptrue% |
56 \isamarkupfalse% |
54 \isamarkupfalse% |
57 \end{isabellebody}% |
55 \end{isabellebody}% |
58 %%% Local Variables: |
56 %%% Local Variables: |