14 le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
14 le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
15 size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
15 size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
16 |
16 |
17 text{*\noindent |
17 text{*\noindent |
18 The infix function @{text"!"} yields the nth element of a list. |
18 The infix function @{text"!"} yields the nth element of a list. |
|
19 |
|
20 \begin{warn} |
|
21 A type constructor can be instantiated in only one way to |
|
22 a given type class. For example, our two instantiations of \isa{list} must |
|
23 reside in separate theories with disjoint scopes.\REMARK{Tobias, please check} |
|
24 \end{warn} |
19 *} |
25 *} |
20 |
26 |
21 subsubsection{*Predefined Overloading*} |
27 subsubsection{*Predefined Overloading*} |
22 |
28 |
23 text{* |
29 text{* |
24 HOL comes with a number of overloaded constants and corresponding classes. |
30 HOL comes with a number of overloaded constants and corresponding classes. |
25 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
31 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
26 defined on all numeric types and sometimes on other types as well, for example |
32 defined on all numeric types and sometimes on other types as well, for example |
27 @{text"-"}, @{text"\<le>"} and @{text"<"} on sets. |
33 $-$ and @{text"\<le>"} on sets. |
28 |
34 |
29 In addition there is a special input syntax for bounded quantifiers: |
35 In addition there is a special input syntax for bounded quantifiers: |
30 \begin{center} |
36 \begin{center} |
31 \begin{tabular}{lcl} |
37 \begin{tabular}{lcl} |
32 @{text"\<forall>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |
38 @{text"\<forall>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |