doc-src/TutorialI/Misc/appendix.thy
author bulwahn
Mon, 22 Mar 2010 08:30:12 +0100
changeset 35876 ac44e2312f0a
parent 31677 799aecc0df56
permissions -rw-r--r--
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31677
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
     1
(*<*)theory appendix
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
     2
imports Main
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
     3
begin(*>*)
10994
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     4
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     5
text{*
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     6
\begin{table}[htbp]
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     7
\begin{center}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     8
\begin{tabular}{lll}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
     9
Constant & Type & Syntax \\
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    10
\hline
31677
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    11
@{term [source] 0} & @{typeof [show_sorts] "0"} \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    12
@{term [source] 1} & @{typeof [show_sorts] "1"} \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    13
@{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    14
@{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    15
@{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    16
@{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    17
@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    18
@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    19
@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    20
@{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    21
@{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    22
@{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    23
@{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    24
@{term [source] top} & @{typeof [show_sorts] "top"} \\
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    25
@{term [source] bot} & @{typeof [show_sorts] "bot"}
10994
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    26
\end{tabular}
31677
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    27
\caption{Important Overloaded Constants in Main}
10994
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    28
\label{tab:overloading}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    29
\end{center}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    30
\end{table}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    31
*}
9429f2e7d16a *** empty log message ***
nipkow
parents:
diff changeset
    32
31677
799aecc0df56 updated table of overloaded constants
haftmann
parents: 24629
diff changeset
    33
(*<*)end(*>*)