35 @{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
35 @{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
36 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
36 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
37 @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
37 @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
38 @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\ |
38 @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\ |
39 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\ |
39 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\ |
40 @{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & $\mid~\mid$\\ |
40 @{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\ |
41 @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
41 @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
42 @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
42 @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
43 @{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
43 @{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
44 @{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} |
44 @{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
|
45 @{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} & |
|
46 @{text LEAST}$~x.~P$ |
45 \end{tabular} |
47 \end{tabular} |
46 \caption{Overloaded constants in HOL} |
48 \caption{Overloaded constants in HOL} |
47 \label{tab:overloading} |
49 \label{tab:overloading} |
48 \end{center} |
50 \end{center} |
49 \end{table} |
51 \end{table} |