doc-src/Main/Docs/Main_Doc.thy
 changeset 35007 8c339c73495c parent 33057 764547b68538 child 35061 be1e25a62ec8
equal inserted replaced
34999:5312d2ffee3b 35007:8c339c73495c
    46 A collection of classes defining basic orderings:
    46 A collection of classes defining basic orderings:
    47 preorder, partial order, linear order, dense linear order and wellorder.
    47 preorder, partial order, linear order, dense linear order and wellorder.
    48 \smallskip
    48 \smallskip
    49
    49
    50 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    50 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    51 @{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
    51 @{const Algebras.less_eq} & @{typeof Algebras.less_eq} & (\verb$<=$)\\
    52 @{const HOL.less} & @{typeof HOL.less}\\
    52 @{const Algebras.less} & @{typeof Algebras.less}\\
    53 @{const Orderings.Least} & @{typeof Orderings.Least}\\
    53 @{const Orderings.Least} & @{typeof Orderings.Least}\\
    54 @{const Orderings.min} & @{typeof Orderings.min}\\
    54 @{const Orderings.min} & @{typeof Orderings.min}\\
    55 @{const Orderings.max} & @{typeof Orderings.max}\\
    55 @{const Orderings.max} & @{typeof Orderings.max}\\
    56 @{const[source] top} & @{typeof Orderings.top}\\
    56 @{const[source] top} & @{typeof Orderings.top}\\
    57 @{const[source] bot} & @{typeof Orderings.bot}\\
    57 @{const[source] bot} & @{typeof Orderings.bot}\\