1.1 --- a/src/HOL/HOL.thy	Thu Oct 04 19:41:55 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 04 19:42:03 2007 +0200
     1.3 @@ -263,16 +263,16 @@
     1.4    less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
     1.5  
     1.6  abbreviation (input)
     1.7 -  greater  (infix "\<^loc>>" 50) where
     1.8 -  "x \<^loc>> y \<equiv> y \<^loc>< x"
     1.9 -
    1.10 -abbreviation (input)
    1.11    greater_eq  (infix "\<^loc>>=" 50) where
    1.12    "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.13  
    1.14  notation (input)
    1.15    greater_eq  (infix "\<^loc>\<ge>" 50)
    1.16  
    1.17 +abbreviation (input)
    1.18 +  greater  (infix "\<^loc>>" 50) where
    1.19 +  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.20 +
    1.21  definition
    1.22    Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
    1.23  where
    1.24 @@ -294,15 +294,12 @@
    1.25    less_eq  ("op \<le>") and
    1.26    less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.27  
    1.28 -abbreviation (input)
    1.29 -  greater  (infix ">" 50) where
    1.30 -  "x > y \<equiv> y < x"
    1.31 -
    1.32 -abbreviation (input)
    1.33 -  greater_eq  (infix ">=" 50) where
    1.34 -  "x >= y \<equiv> y <= x"
    1.35 +notation (input)
    1.36 +  greater  (infix ">" 50)
    1.37  
    1.38  notation (input)
    1.39 +  greater_eq  (infix ">=" 50)
    1.40 +and
    1.41    greater_eq  (infix "\<ge>" 50)
    1.42  
    1.43  syntax