--- 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 ("(_/ \\<le> _)" [50, 51] 50)
+ "op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
+
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
-