# HG changeset patch
# User haftmann
# Date 1191519723 -7200
# Node ID 2bdf31a97362c411a47e4fe0aaf2af1bf8ba26e4
# Parent  df8448bc7a8b9b2006d7f9f498aa76d58baa0369
clarified declarations in class ord

diff -r df8448bc7a8b -r 2bdf31a97362 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 04 19:41:55 2007 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 04 19:42:03 2007 +0200
@@ -263,16 +263,16 @@
   less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater  (infix "\<^loc>>" 50) where
-  "x \<^loc>> y \<equiv> y \<^loc>< x"
-
-abbreviation (input)
   greater_eq  (infix "\<^loc>>=" 50) where
   "x \<^loc>>= y \<equiv> y \<^loc><= x"
 
 notation (input)
   greater_eq  (infix "\<^loc>\<ge>" 50)
 
+abbreviation (input)
+  greater  (infix "\<^loc>>" 50) where
+  "x \<^loc>> y \<equiv> y \<^loc>< x"
+
 definition
   Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
 where
@@ -294,15 +294,12 @@
   less_eq  ("op \<le>") and
   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
-
-abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
+notation (input)
+  greater  (infix ">" 50)
 
 notation (input)
+  greater_eq  (infix ">=" 50)
+and
   greater_eq  (infix "\<ge>" 50)
 
 syntax