src/HOL/Ord.thy
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