src/HOL/Ord.thy
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1370 7361ac9b024d
child 2006 72754e060aa2
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
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
clasohm@1370
    15
  "<", "<="     :: ['a::ord, 'a] => bool              (infixl 50)
clasohm@1370
    16
  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
clasohm@1370
    17
  min, max      :: ['a::ord, 'a] => 'a
clasohm@923
    18
clasohm@923
    19
defs
clasohm@923
    20
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
clasohm@965
    21
  min_def       "min a b == (if a <= b then a else b)"
clasohm@965
    22
  max_def       "max a b == (if a <= b then b else a)"
clasohm@923
    23
clasohm@923
    24
end
clasohm@923
    25