1.1 --- a/src/HOL/Orderings.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -11,6 +11,41 @@
     1.4    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
     1.5  begin
     1.6  
     1.7 +subsection {* Syntactic orders *}
     1.8 +
     1.9 +class ord =
    1.10 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.12 +begin
    1.13 +
    1.14 +notation
    1.15 +  less_eq  ("op <=") and
    1.16 +  less_eq  ("(_/ <= _)" [51, 51] 50) and
    1.17 +  less  ("op <") and
    1.18 +  less  ("(_/ < _)"  [51, 51] 50)
    1.19 +  
    1.20 +notation (xsymbols)
    1.21 +  less_eq  ("op \<le>") and
    1.22 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.23 +
    1.24 +notation (HTML output)
    1.25 +  less_eq  ("op \<le>") and
    1.26 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.27 +
    1.28 +abbreviation (input)
    1.29 +  greater_eq  (infix ">=" 50) where
    1.30 +  "x >= y \<equiv> y <= x"
    1.31 +
    1.32 +notation (input)
    1.33 +  greater_eq  (infix "\<ge>" 50)
    1.34 +
    1.35 +abbreviation (input)
    1.36 +  greater  (infix ">" 50) where
    1.37 +  "x > y \<equiv> y < x"
    1.38 +
    1.39 +end
    1.40 +
    1.41 +
    1.42  subsection {* Quasi orders *}
    1.43  
    1.44  class preorder = ord +