--- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{2}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-Of course this is not the only possible definition of the two relations.
-Componentwise comparison of lists of equal length also makes sense. This time
-the elements of the list must also be of class \isa{ordrel} to permit their
-comparison:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
-
-\begin{warn}
-A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Predefined Overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
-defined on all numeric types and sometimes on other types as well, for example
-$-$ and \isa{{\isasymle}} on sets.
-
-In addition there is a special syntax for bounded quantifiers:
-\begin{center}
-\begin{tabular}{lcl}
-\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
-\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
-\end{tabular}
-\end{center}
-And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: