src/Doc/Tutorial/Misc/appendix.thy
author haftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 60429 d3d1e185cd63
parent 48985 5386df44a037
child 63950 cdc1e59aa513
permissions -rw-r--r--
uniform _ div _ as infix syntax for ring division
haftmann@31677
     1
(*<*)theory appendix
haftmann@31677
     2
imports Main
haftmann@31677
     3
begin(*>*)
nipkow@10994
     4
nipkow@10994
     5
text{*
nipkow@10994
     6
\begin{table}[htbp]
nipkow@10994
     7
\begin{center}
nipkow@10994
     8
\begin{tabular}{lll}
nipkow@10994
     9
Constant & Type & Syntax \\
nipkow@10994
    10
\hline
haftmann@31677
    11
@{term [source] 0} & @{typeof [show_sorts] "0"} \\
haftmann@31677
    12
@{term [source] 1} & @{typeof [show_sorts] "1"} \\
haftmann@31677
    13
@{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\
haftmann@31677
    14
@{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
haftmann@31677
    15
@{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
haftmann@31677
    16
@{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
haftmann@60429
    17
@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
haftmann@60429
    18
@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
haftmann@31677
    19
@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
haftmann@31677
    20
@{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
haftmann@31677
    21
@{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
haftmann@31677
    22
@{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
haftmann@31677
    23
@{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\
haftmann@31677
    24
@{term [source] top} & @{typeof [show_sorts] "top"} \\
haftmann@31677
    25
@{term [source] bot} & @{typeof [show_sorts] "bot"}
nipkow@10994
    26
\end{tabular}
haftmann@31677
    27
\caption{Important Overloaded Constants in Main}
nipkow@10994
    28
\label{tab:overloading}
nipkow@10994
    29
\end{center}
nipkow@10994
    30
\end{table}
nipkow@10994
    31
*}
nipkow@10994
    32
haftmann@31677
    33
(*<*)end(*>*)