# HG changeset patch
# User wenzelm
# Date 849109699 -3600
# Node ID e6d738f2b9a9ae0b9b1649dc0b292e67a762b687
# Parent  8ad8ee759d9fba34967a914e05f366d833cb4c12
fixed comment;
added "op <", "op <=" syntax;
added symbol syntax;

diff -r 8ad8ee759d9f -r e6d738f2b9a9 src/HOL/Ord.thy
--- 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
-