equal
deleted
inserted
replaced
6 We start with a concept that is required for type classes but already |
6 We start with a concept that is required for type classes but already |
7 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
7 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
8 constant may have multiple definitions at non-overlapping types.% |
8 constant may have multiple definitions at non-overlapping types.% |
9 \end{isamarkuptext}% |
9 \end{isamarkuptext}% |
10 % |
10 % |
11 \isamarkupsubsubsection{An initial example} |
11 \isamarkupsubsubsection{An initial example% |
|
12 } |
12 % |
13 % |
13 \begin{isamarkuptext}% |
14 \begin{isamarkuptext}% |
14 If we want to introduce the notion of an \emph{inverse} for arbitrary types we |
15 If we want to introduce the notion of an \emph{inverse} for arbitrary types we |
15 give it a polymorphic type% |
16 give it a polymorphic type% |
16 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |