src/HOL/Ord.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 2006 72754e060aa2
child 2259 e6d738f2b9a9
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
clasohm@923
     1
(*  Title:      HOL/Ord.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
The type class for ordered types    (* FIXME improve comment *)
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
Ord = HOL +
clasohm@923
    10
clasohm@923
    11
axclass
clasohm@923
    12
  ord < term
clasohm@923
    13
clasohm@923
    14
consts
paulson@2006
    15
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50,51] 50)
paulson@2006
    16
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50,51] 50)
clasohm@1370
    17
  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
clasohm@1370
    18
  min, max      :: ['a::ord, 'a] => 'a
clasohm@923
    19
clasohm@923
    20
defs
clasohm@923
    21
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
clasohm@965
    22
  min_def       "min a b == (if a <= b then a else b)"
clasohm@965
    23
  max_def       "max a b == (if a <= b then b else a)"
clasohm@923
    24
clasohm@923
    25
end
clasohm@923
    26