isabelle: src/Doc/Tutorial/Misc/appendix.thy@23307fd33906 (annotated)

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
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 63950 diff changeset	5	text\<open>
10994 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) \\
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 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}
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 63950 diff changeset	31	\<close>
10994 9429f2e7d16a * empty log message * nipkow parents: diff changeset	32
31677 799aecc0df56 updated table of overloaded constants haftmann parents: 24629 diff changeset	33	(<)end(>)

author	wenzelm
	Fri, 12 Jan 2018 14:08:53 +0100
changeset 67406	23307fd33906
parent 63950	cdc1e59aa513
permissions	-rw-r--r--