10994
|
1 |
(*<*)
|
16417
|
2 |
theory appendix imports Main begin;
|
10994
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*
|
|
6 |
\begin{table}[htbp]
|
|
7 |
\begin{center}
|
|
8 |
\begin{tabular}{lll}
|
|
9 |
Constant & Type & Syntax \\
|
|
10 |
\hline
|
12332
|
11 |
@{text 0} & @{text "'a::zero"} \\
|
|
12 |
@{text 1} & @{text "'a::one"} \\
|
10994
|
13 |
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
|
|
14 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
|
|
15 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
|
|
16 |
@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
|
|
17 |
@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
|
|
18 |
@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
|
|
19 |
@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
|
|
20 |
@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
|
|
21 |
@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
|
|
22 |
@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
|
|
23 |
@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
|
|
24 |
@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
|
|
25 |
@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
|
|
26 |
@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
|
|
27 |
@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
|
|
28 |
@{text LEAST}$~x.~P$
|
|
29 |
\end{tabular}
|
|
30 |
\caption{Overloaded Constants in HOL}
|
|
31 |
\label{tab:overloading}
|
|
32 |
\end{center}
|
|
33 |
\end{table}
|
|
34 |
*}
|
|
35 |
|
|
36 |
(*<*)
|
|
37 |
end
|
|
38 |
(*>*)
|