Mercurial Mercurial > repos > Old_HOL / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Ord.thy
author lcp
Tue, 06 Sep 1994 10:56:54 +0200
changeset 135 a06a2d930a03
parent 118 5b96b1252cdc
child 145 a9f7ff3a464c
permissions -rw-r--r--
HOL/ex/PropLog.thy: tidied

(*  Title: 	HOL/Ord.thy
    ID:         $Id$
    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

The type class for ordered types
*)

Ord = HOL +
classes
  ord < term
consts
  "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
  mono		:: "['a::ord => 'b::ord] => bool"       (*monotonicity*)
  min,max	:: "['a::ord,'a] => 'a"

rules

mono_def  "mono(f)  == (!A B. A <= B --> f(A) <= f(B))"
min_def   "min(a,b) == if(a <= b, a, b)"
max_def   "max(a,b) == if(a <= b, b, a)"

end
Old_HOL