isabelle: src/Doc/Tutorial/Misc/appendix.thy@76130b7cc450 (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
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) \\
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) \\
31677 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(>)

author	eberlm
	Wed, 25 May 2016 12:24:00 +0200
changeset 63144	76130b7cc450
parent 60429	d3d1e185cd63
child 63950	cdc1e59aa513
permissions	-rw-r--r--