src/HOL/Orderings.thy
changeset 35092 cfe605c54e50
parent 35028 108662d50512
child 35115 446c5063e4fd
--- a/src/HOL/Orderings.thy	Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Orderings.thy	Wed Feb 10 14:12:04 2010 +0100
@@ -11,6 +11,41 @@
   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
 begin
 
+subsection {* Syntactic orders *}
+
+class ord =
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+
+notation
+  less_eq  ("op <=") and
+  less_eq  ("(_/ <= _)" [51, 51] 50) and
+  less  ("op <") and
+  less  ("(_/ < _)"  [51, 51] 50)
+  
+notation (xsymbols)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+notation (HTML output)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
+  "x >= y \<equiv> y <= x"
+
+notation (input)
+  greater_eq  (infix "\<ge>" 50)
+
+abbreviation (input)
+  greater  (infix ">" 50) where
+  "x > y \<equiv> y < x"
+
+end
+
+
 subsection {* Quasi orders *}
 
 class preorder = ord +