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)
```