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
     1 (*  Title:      HOL/Ord.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The type class for ordered types    (* FIXME improve comment *)
     7 *)
     8 
     9 Ord = HOL +
    10 
    11 axclass
    12   ord < term
    13 
    14 consts
    15   "<", "<="     :: ['a::ord, 'a] => bool              (infixl 50)
    16   mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
    17   min, max      :: ['a::ord, 'a] => 'a
    18 
    19 defs
    20   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    21   min_def       "min a b == (if a <= b then a else b)"
    22   max_def       "max a b == (if a <= b then b else a)"
    23 
    24 end
    25