src/HOL/Orderings.thy
changeset 20714 6a122dba034c
parent 20588 c847c56edf0c
child 21044 9690be52ee5d
     1.1 --- a/src/HOL/Orderings.thy	Tue Sep 26 13:34:16 2006 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Sep 26 13:34:17 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  subsection {* Order signatures and orders *}
     1.5  
     1.6  class ord = eq +
     1.7 -  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.8 +  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (*FIXME: class_package should do the job*)
     1.9    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10    fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11  
    1.12 @@ -33,15 +33,44 @@
    1.13    less_eq  ("op \<le>")
    1.14    less_eq  ("(_/ \<le> _)"  [50, 51] 50)
    1.15  
    1.16 +
    1.17 +abbreviation (in ord)
    1.18 +  "less_eq_syn \<equiv> less_eq"
    1.19 +  "less_syn \<equiv> less"
    1.20 +
    1.21 +const_syntax (in ord) 
    1.22 +  less_eq_syn  ("op \<^loc><=")
    1.23 +  less_eq_syn  ("(_/ \<^loc><= _)" [50, 51] 50)
    1.24 +  less_syn  ("op \<^loc><")
    1.25 +  less_syn  ("(_/ \<^loc>< _)"  [50, 51] 50)
    1.26 +  
    1.27 +const_syntax (in ord) (xsymbols)
    1.28 +  less_eq_syn  ("op \<^loc>\<le>")
    1.29 +  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.30 +
    1.31 +const_syntax (in ord) (HTML output)
    1.32 +  less_eq_syn  ("op \<^loc>\<le>")
    1.33 +  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
    1.34 +
    1.35 +
    1.36  abbreviation (input)
    1.37    greater  (infixl ">" 50)
    1.38 -  "x > y == y < x"
    1.39 +  "x > y \<equiv> y < x"
    1.40    greater_eq  (infixl ">=" 50)
    1.41 -  "x >= y == y <= x"
    1.42 -
    1.43 +  "x >= y \<equiv> y <= x"
    1.44 +  
    1.45  const_syntax (xsymbols)
    1.46    greater_eq  (infixl "\<ge>" 50)
    1.47  
    1.48 +abbreviation (in ord) (input)
    1.49 +  greater  (infix "\<^loc>>" 50)
    1.50 +  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.51 +  greater_eq  (infix "\<^loc>>=" 50)
    1.52 +  "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.53 +
    1.54 +const_syntax (in ord) (xsymbols)
    1.55 +  greater_eq  (infixl "\<^loc>\<ge>" 50)
    1.56 +
    1.57  
    1.58  subsection {* Monotonicity *}
    1.59