equal
deleted
inserted
replaced
1 (*<*)theory appendix |
|
2 imports Main |
|
3 begin(*>*) |
|
4 |
|
5 text{* |
|
6 \begin{table}[htbp] |
|
7 \begin{center} |
|
8 \begin{tabular}{lll} |
|
9 Constant & Type & Syntax \\ |
|
10 \hline |
|
11 @{term [source] 0} & @{typeof [show_sorts] "0"} \\ |
|
12 @{term [source] 1} & @{typeof [show_sorts] "1"} \\ |
|
13 @{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\ |
|
14 @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\ |
|
15 @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\ |
|
16 @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\ |
|
17 @{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\ |
|
18 @{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\ |
|
19 @{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\ |
|
20 @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\ |
|
21 @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\ |
|
22 @{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\ |
|
23 @{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\ |
|
24 @{term [source] top} & @{typeof [show_sorts] "top"} \\ |
|
25 @{term [source] bot} & @{typeof [show_sorts] "bot"} |
|
26 \end{tabular} |
|
27 \caption{Important Overloaded Constants in Main} |
|
28 \label{tab:overloading} |
|
29 \end{center} |
|
30 \end{table} |
|
31 *} |
|
32 |
|
33 (*<*)end(*>*) |
|