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