src/HOL/Orderings.thy
changeset 61955 e96292f32c3c
parent 61824 dcbe9f756ae0
child 62521 6383440f41a8
     1.1 --- a/src/HOL/Orderings.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -93,25 +93,25 @@
     1.4  begin
     1.5  
     1.6  notation
     1.7 -  less_eq  ("op <=") and
     1.8 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
     1.9 +  less_eq  ("op \<le>") and
    1.10 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50) and
    1.11    less  ("op <") and
    1.12    less  ("(_/ < _)"  [51, 51] 50)
    1.13  
    1.14 -notation (xsymbols)
    1.15 -  less_eq  ("op \<le>") and
    1.16 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.17 +abbreviation (input)
    1.18 +  greater_eq  (infix "\<ge>" 50)
    1.19 +  where "x \<ge> y \<equiv> y \<le> x"
    1.20  
    1.21  abbreviation (input)
    1.22 -  greater_eq  (infix ">=" 50) where
    1.23 -  "x >= y \<equiv> y <= x"
    1.24 +  greater  (infix ">" 50)
    1.25 +  where "x > y \<equiv> y < x"
    1.26 +
    1.27 +notation (ASCII)
    1.28 +  less_eq  ("op <=") and
    1.29 +  less_eq  ("(_/ <= _)" [51, 51] 50)
    1.30  
    1.31  notation (input)
    1.32 -  greater_eq  (infix "\<ge>" 50)
    1.33 -
    1.34 -abbreviation (input)
    1.35 -  greater  (infix ">" 50) where
    1.36 -  "x > y \<equiv> y < x"
    1.37 +  greater_eq  (infix ">=" 50)
    1.38  
    1.39  end
    1.40  
    1.41 @@ -652,7 +652,7 @@
    1.42  
    1.43  subsection \<open>Bounded quantifiers\<close>
    1.44  
    1.45 -syntax
    1.46 +syntax (ASCII)
    1.47    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3ALL _<_./ _)"  [0, 0, 10] 10)
    1.48    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3EX _<_./ _)"  [0, 0, 10] 10)
    1.49    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _<=_./ _)" [0, 0, 10] 10)
    1.50 @@ -663,7 +663,7 @@
    1.51    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
    1.52    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
    1.53  
    1.54 -syntax (xsymbols)
    1.55 +syntax
    1.56    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
    1.57    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
    1.58    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)