# HG changeset patch
# User wenzelm
# Date 1165353279 -3600
# Node ID 43d709faa9dc8bc06c7d4da82992c532d0159d4a
# Parent  01b2d13153c8c608efb98480fcdecea8e14c2b94
restored notation for less/less_eq (observe proper order of mixfix annotations!);
simplified notation for greater/greater_eq, which is only used for input;
removed duplicate abbreviations (implicit inheritance);

diff -r 01b2d13153c8 -r 43d709faa9dc src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Dec 05 22:04:24 2006 +0100
+++ b/src/HOL/Orderings.thy	Tue Dec 05 22:14:39 2006 +0100
@@ -14,15 +14,15 @@
 subsection {* Order syntax *}
 
 class ord =
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infix "\<sqsubset>" 50)
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
 begin
 
 notation
+  less_eq  ("op \<^loc><=") and
   less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
-  less_eq  ("op \<^loc><=") and
-  less  ("(_/ \<^loc>< _)"  [51, 51] 50) and
-  less  ("op \<^loc><")
+  less  ("op \<^loc><") and
+  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
   
 notation (xsymbols)
   less_eq  ("op \<^loc>\<le>") and
@@ -33,32 +33,23 @@
   less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater_eq  ("(_/ \<^loc>>= _)" [51, 51] 50) where
-  "x \<^loc>>= y \<equiv> y \<^loc><= x"
-
-abbreviation (input)
-  greater  ("(_/ \<^loc>> _)" [51, 51] 50) where
+  greater  (infix "\<^loc>>" 50) where
   "x \<^loc>> y \<equiv> y \<^loc>< x"
 
-notation
-  greater_eq  ("op \<^loc>>=") and
-  greater  ("op \<^loc>>")
+abbreviation (input)
+  greater_eq  (infix "\<^loc>>=" 50) where
+  "x \<^loc>>= y \<equiv> y \<^loc><= x"
 
-notation (xsymbols)
-  greater_eq  ("op \<^loc>\<ge>") and
-  greater_eq  ("(_/ \<^loc>\<ge> _)"  [51, 51] 50)
-
-notation (HTML output)
-  greater_eq  ("op \<^loc>\<ge>") and
-  greater_eq  ("(_/ \<^loc>\<ge> _)"  [51, 51] 50)
+notation (input)
+  greater_eq  (infix "\<^loc>\<ge>" 50)
 
 end
 
 notation
+  less_eq  ("op <=") and
   less_eq  ("(_/ <= _)" [51, 51] 50) and
-  less_eq  ("op <=") and
-  less  ("(_/ < _)"  [51, 51] 50) and
-  less  ("op <")
+  less  ("op <") and
+  less  ("(_/ < _)"  [51, 51] 50)
   
 notation (xsymbols)
   less_eq  ("op \<le>") and
@@ -69,24 +60,15 @@
   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater_eq  ("(_/ >= _)" [51, 51] 50) where
-  "x >= y \<equiv> y <= x"
-
-abbreviation (input)
-  greater  ("(_/ > _)" [51, 51] 50) where
+  greater  (infix ">" 50) where
   "x > y \<equiv> y < x"
 
-notation
-  greater_eq  ("op >=") and
-  greater  ("op >")
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
+  "x >= y \<equiv> y <= x"
 
-notation (xsymbols)
-  greater_eq  ("op \<ge>") and
-  greater_eq  ("(_/ \<ge> _)"  [51, 51] 50)
-
-notation (HTML output)
-  greater_eq  ("op \<ge>") and
-  greater_eq  ("(_/ \<ge> _)"  [51, 51] 50)
+notation (input)
+  greater_eq  (infix "\<ge>" 50)
 
 
 subsection {* Quasiorders (preorders) *}
@@ -97,14 +79,6 @@
   and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 begin
 
-abbreviation (input)
-  greater_eq  (infixl "\<^loc>\<ge>" 50) where
-  "x \<^loc>\<ge> y \<equiv> y \<sqsubseteq> x"
-
-abbreviation (input)
-  greater (infixl "\<^loc>>" 50) where
-  "x \<^loc>> y \<equiv> y \<sqsubset> x"
-
 text {* Reflexivity. *}
 
 lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"