changeset 2006 | 72754e060aa2 |
parent 1370 | 7361ac9b024d |
child 2259 | e6d738f2b9a9 |
--- a/src/HOL/Ord.thy Mon Sep 23 17:46:12 1996 +0200 +++ b/src/HOL/Ord.thy Mon Sep 23 17:47:49 1996 +0200 @@ -12,7 +12,8 @@ ord < term consts - "<", "<=" :: ['a::ord, 'a] => bool (infixl 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