# HG changeset patch # User wenzelm # Date 849109699 -3600 # Node ID e6d738f2b9a9ae0b9b1649dc0b292e67a762b687 # Parent 8ad8ee759d9fba34967a914e05f366d833cb4c12 fixed comment; added "op <", "op <=" syntax; added symbol syntax; diff -r 8ad8ee759d9f -r e6d738f2b9a9 src/HOL/Ord.thy --- a/src/HOL/Ord.thy Wed Nov 27 16:45:57 1996 +0100 +++ b/src/HOL/Ord.thy Wed Nov 27 16:48:19 1996 +0100 @@ -3,7 +3,7 @@ Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -The type class for ordered types (* FIXME improve comment *) +Type class for order signatures. *) Ord = HOL + @@ -12,15 +12,22 @@ ord < term consts - "op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50,51] 50) - "op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50,51] 50) + "op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50) + "op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50) mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) min, max :: ['a::ord, 'a] => 'a +syntax + "op <" :: ['a::ord, 'a] => bool ("op <") + "op <=" :: ['a::ord, 'a] => bool ("op <=") + +syntax (symbols) + "op <=" :: ['a::ord, 'a] => bool ("(_/ \\ _)" [50, 51] 50) + "op <=" :: ['a::ord, 'a] => bool ("op \\") + defs mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" min_def "min a b == (if a <= b then a else b)" max_def "max a b == (if a <= b then b else a)" end -