# HG changeset patch
# User haftmann
# Date 1159270457 -7200
# Node ID 6a122dba034cb8f753821671c78fb00022432c41
# Parent  823967ef47f17339388c5b41ba10b188ca0e166d
tuned syntax for <= <

diff -r 823967ef47f1 -r 6a122dba034c src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Sep 26 13:34:16 2006 +0200
+++ b/src/HOL/Orderings.thy	Tue Sep 26 13:34:17 2006 +0200
@@ -15,7 +15,7 @@
 subsection {* Order signatures and orders *}
 
 class ord = eq +
-  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (*FIXME: class_package should do the job*)
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
@@ -33,15 +33,44 @@
   less_eq  ("op \<le>")
   less_eq  ("(_/ \<le> _)"  [50, 51] 50)
 
+
+abbreviation (in ord)
+  "less_eq_syn \<equiv> less_eq"
+  "less_syn \<equiv> less"
+
+const_syntax (in ord) 
+  less_eq_syn  ("op \<^loc><=")
+  less_eq_syn  ("(_/ \<^loc><= _)" [50, 51] 50)
+  less_syn  ("op \<^loc><")
+  less_syn  ("(_/ \<^loc>< _)"  [50, 51] 50)
+  
+const_syntax (in ord) (xsymbols)
+  less_eq_syn  ("op \<^loc>\<le>")
+  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
+
+const_syntax (in ord) (HTML output)
+  less_eq_syn  ("op \<^loc>\<le>")
+  less_eq_syn  ("(_/ \<^loc>\<le> _)"  [50, 51] 50)
+
+
 abbreviation (input)
   greater  (infixl ">" 50)
-  "x > y == y < x"
+  "x > y \<equiv> y < x"
   greater_eq  (infixl ">=" 50)
-  "x >= y == y <= x"
-
+  "x >= y \<equiv> y <= x"
+  
 const_syntax (xsymbols)
   greater_eq  (infixl "\<ge>" 50)
 
+abbreviation (in ord) (input)
+  greater  (infix "\<^loc>>" 50)
+  "x \<^loc>> y \<equiv> y \<^loc>< x"
+  greater_eq  (infix "\<^loc>>=" 50)
+  "x \<^loc>>= y \<equiv> y \<^loc><= x"
+
+const_syntax (in ord) (xsymbols)
+  greater_eq  (infixl "\<^loc>\<ge>" 50)
+
 
 subsection {* Monotonicity *}