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