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