| author | wenzelm |
| Thu, 29 Jun 2017 21:43:55 +0200 | |
| changeset 66223 | a6fdb22b0ce2 |
| parent 63950 | cdc1e59aa513 |
| child 67406 | 23307fd33906 |
| permissions | -rw-r--r-- |
| 31677 | 1 |
(*<*)theory appendix |
2 |
imports Main |
|
3 |
begin(*>*) |
|
| 10994 | 4 |
|
5 |
text{*
|
|
6 |
\begin{table}[htbp]
|
|
7 |
\begin{center}
|
|
8 |
\begin{tabular}{lll}
|
|
9 |
Constant & Type & Syntax \\ |
|
10 |
\hline |
|
| 31677 | 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) \\
|
|
|
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
48985
diff
changeset
|
17 |
@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
|
|
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
48985
diff
changeset
|
18 |
@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
|
|
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
60429
diff
changeset
|
19 |
@{term [source] modulo} & @{typeof [show_sorts] "modulo"} & (infixl $mod$ 70) \\
|
| 31677 | 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"}
|
|
| 10994 | 26 |
\end{tabular}
|
| 31677 | 27 |
\caption{Important Overloaded Constants in Main}
|
| 10994 | 28 |
\label{tab:overloading}
|
29 |
\end{center}
|
|
30 |
\end{table}
|
|
31 |
*} |
|
32 |
||
| 31677 | 33 |
(*<*)end(*>*) |