| changeset 1370 | 7361ac9b024d |
| parent 965 | 24eef3860714 |
| child 2006 | 72754e060aa2 |
--- a/src/HOL/Ord.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Ord.thy Wed Nov 29 16:44:59 1995 +0100 @@ -12,9 +12,9 @@ ord < term consts - "<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) - mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) - min, max :: "['a::ord, 'a] => 'a" + "<", "<=" :: ['a::ord, 'a] => bool (infixl 50) + mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) + min, max :: ['a::ord, 'a] => 'a defs mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"