1.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Dec 18 16:11:53 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Dec 18 16:45:17 2000 +0100
     1.3 @@ -48,7 +48,18 @@
     1.4  \caption{Overloaded constants in HOL}
     1.5  \label{tab:overloading}
     1.6  \end{center}
     1.7 -\end{table}%
     1.8 +\end{table}
     1.9 +
    1.10 +In addition there is a special input syntax for bounded quantifiers:
    1.11 +\begin{center}
    1.12 +\begin{tabular}{lcl}
    1.13 +\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
    1.14 +\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
    1.15 +\end{tabular}
    1.16 +\end{center}
    1.17 +And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
    1.18 +The form on the left is translated into the one on the right upon input but it is not
    1.19 +translated back upon output.%
    1.20  \end{isamarkuptext}%
    1.21  \end{isabellebody}%
    1.22  %%% Local Variables: