# HG changeset patch
# User wenzelm
# Date 1163069893 -3600
# Node ID 63ab016c99ca461559b17fc5983b91903d7eae53
# Parent  62f25a96f0c1cf6f07aa0e226befe7b2782d26a2
modified less/less_eq syntax to avoid "x < y < z" etc.;

diff -r 62f25a96f0c1 -r 63ab016c99ca src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Nov 09 00:43:12 2006 +0100
+++ b/src/HOL/Orderings.thy	Thu Nov 09 11:58:13 2006 +0100
@@ -20,17 +20,17 @@
 
 notation
   less_eq  ("op \<^loc><=")
-  less_eq  ("(_/ \<^loc><= _)" [50, 51] 50)
+  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50)
   less  ("op \<^loc><")
-  less  ("(_/ \<^loc>< _)"  [50, 51] 50)
+  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
 
 notation (xsymbols)
   less_eq  ("op \<^loc>\<le>")
-  less_eq  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
+  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 notation (HTML output)
   less_eq  ("op \<^loc>\<le>")
-  less_eq  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
+  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 abbreviation (input)
   greater  (infix "\<^loc>>" 50)
@@ -39,32 +39,32 @@
   "x \<^loc>>= y \<equiv> y \<^loc><= x"
 
 notation (xsymbols)
-  greater_eq  (infixl "\<^loc>\<ge>" 50)
+  greater_eq  (infix "\<^loc>\<ge>" 50)
 
 end
 
 notation
   less_eq  ("op <=")
-  less_eq  ("(_/ <= _)" [50, 51] 50)
+  less_eq  ("(_/ <= _)" [51, 51] 50)
   less  ("op <")
-  less  ("(_/ < _)"  [50, 51] 50)
+  less  ("(_/ < _)"  [51, 51] 50)
   
 notation (xsymbols)
   less_eq  ("op \<le>")
-  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 notation (HTML output)
   less_eq  ("op \<le>")
-  less_eq  ("(_/ \<le> _)"  [50, 51] 50)
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater  (infixl ">" 50)
+  greater  (infix ">" 50)
   "x > y \<equiv> y < x"
-  greater_eq  (infixl ">=" 50)
+  greater_eq  (infix ">=" 50)
   "x >= y \<equiv> y <= x"
   
 notation (xsymbols)
-  greater_eq  (infixl "\<ge>" 50)
+  greater_eq  (infix "\<ge>" 50)
 
 
 subsection {* Partial orderings *}