--- a/src/HOL/Ord.thy Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/Ord.thy Thu Oct 09 15:03:06 1997 +0200
@@ -11,6 +11,10 @@
axclass
ord < term
+syntax
+ "op <" :: ['a::ord, 'a] => bool ("op <")
+ "op <=" :: ['a::ord, 'a] => bool ("op <=")
+
consts
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50)
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50)
@@ -19,13 +23,10 @@
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10)
-syntax
- "op <" :: ['a::ord, 'a] => bool ("op <")
- "op <=" :: ['a::ord, 'a] => bool ("op <=")
+syntax (symbols)
+ "op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
+ "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
-syntax (symbols)
- "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
- "op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
defs
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"