1.1 --- a/src/HOL/Orderings.thy	Tue Nov 07 11:46:45 2006 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Nov 07 11:46:46 2006 +0100
     1.3 @@ -15,60 +15,57 @@
     1.4  
     1.5  class ord =
     1.6    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.7 -  fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.8 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 +begin
    1.10  
    1.11 -const_syntax
    1.12 +notation
    1.13 +  less_eq  ("op \<^loc><=")
    1.14 +  less_eq  ("(_/ \<^loc><= _)" [50, 51] 50)
    1.15 +  less  ("op \<^loc><")
    1.16 +  less  ("(_/ \<^loc>< _)"  [50, 51] 50)
    1.17 +
    1.18 +notation (xsymbols)
    1.19 +  less_eq  ("op \<^loc>\<le>")
    1.20 +  less_eq  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.21 +
    1.22 +notation (HTML output)
    1.23 +  less_eq  ("op \<^loc>\<le>")
    1.24 +  less_eq  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.25 +
    1.26 +abbreviation (input)
    1.27 +  greater  (infix "\<^loc>>" 50)
    1.28 +  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.29 +  greater_eq  (infix "\<^loc>>=" 50)
    1.30 +  "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.31 +
    1.32 +notation (xsymbols)
    1.33 +  greater_eq  (infixl "\<^loc>\<ge>" 50)
    1.34 +
    1.35 +end
    1.36 +
    1.37 +notation
    1.38 +  less_eq  ("op <=")
    1.39 +  less_eq  ("(_/ <= _)" [50, 51] 50)
    1.40    less  ("op <")
    1.41    less  ("(_/ < _)"  [50, 51] 50)
    1.42 -  less_eq  ("op <=")
    1.43 -  less_eq  ("(_/ <= _)" [50, 51] 50)
    1.44 -
    1.45 -const_syntax (xsymbols)
    1.46 +  
    1.47 +notation (xsymbols)
    1.48    less_eq  ("op \<le>")
    1.49    less_eq  ("(_/ \<le> _)"  [50, 51] 50)
    1.50  
    1.51 -const_syntax (HTML output)
    1.52 +notation (HTML output)
    1.53    less_eq  ("op \<le>")
    1.54    less_eq  ("(_/ \<le> _)"  [50, 51] 50)
    1.55  
    1.56 -
    1.57 -abbreviation (in ord)
    1.58 -  "less_eq_syn \<equiv> less_eq"
    1.59 -  "less_syn \<equiv> less"
    1.60 -
    1.61 -const_syntax (in ord) 
    1.62 -  less_eq_syn  ("op \<^loc><=")
    1.63 -  less_eq_syn  ("(_/ \<^loc><= _)" [50, 51] 50)
    1.64 -  less_syn  ("op \<^loc><")
    1.65 -  less_syn  ("(_/ \<^loc>< _)"  [50, 51] 50)
    1.66 -  
    1.67 -const_syntax (in ord) (xsymbols)
    1.68 -  less_eq_syn  ("op \<^loc>\<le>")
    1.69 -  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.70 -
    1.71 -const_syntax (in ord) (HTML output)
    1.72 -  less_eq_syn  ("op \<^loc>\<le>")
    1.73 -  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.74 -
    1.75 -
    1.76  abbreviation (input)
    1.77    greater  (infixl ">" 50)
    1.78    "x > y \<equiv> y < x"
    1.79    greater_eq  (infixl ">=" 50)
    1.80    "x >= y \<equiv> y <= x"
    1.81    
    1.82 -const_syntax (xsymbols)
    1.83 +notation (xsymbols)
    1.84    greater_eq  (infixl "\<ge>" 50)
    1.85  
    1.86 -abbreviation (in ord) (input)
    1.87 -  greater  (infix "\<^loc>>" 50)
    1.88 -  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.89 -  greater_eq  (infix "\<^loc>>=" 50)
    1.90 -  "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.91 -
    1.92 -const_syntax (in ord) (xsymbols)
    1.93 -  greater_eq  (infixl "\<^loc>\<ge>" 50)
    1.94 -
    1.95  
    1.96  subsection {* Partial orderings *}
    1.97