doc-src/Main/Docs/Main_Doc.thy
changeset 35277 f228929a6fab
parent 35061 be1e25a62ec8
child 35805 1c4a8d3b26d2
equal deleted inserted replaced
35276:587c893049e1 35277:f228929a6fab
    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 Algebras.less_eq} & @{typeof Algebras.less_eq} & (\verb$<=$)\\
    51 @{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\
    52 @{const Algebras.less} & @{typeof Algebras.less}\\
    52 @{const Orderings.less} & @{typeof Orderings.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}\\