author haftmann Thu, 04 Oct 2007 19:42:03 +0200 changeset 24842 2bdf31a97362 parent 24841 df8448bc7a8b child 24843 0fc73c4003ac
clarified declarations in class ord
 src/HOL/HOL.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/HOL.thy	Thu Oct 04 19:41:55 2007 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 04 19:42:03 2007 +0200
@@ -263,16 +263,16 @@
less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)

abbreviation (input)
-  greater  (infix "\<^loc>>" 50) where
-  "x \<^loc>> y \<equiv> y \<^loc>< x"
-
-abbreviation (input)
greater_eq  (infix "\<^loc>>=" 50) where
"x \<^loc>>= y \<equiv> y \<^loc><= x"

notation (input)
greater_eq  (infix "\<^loc>\<ge>" 50)

+abbreviation (input)
+  greater  (infix "\<^loc>>" 50) where
+  "x \<^loc>> y \<equiv> y \<^loc>< x"
+
definition
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
where
@@ -294,15 +294,12 @@
less_eq  ("op \<le>") and
less_eq  ("(_/ \<le> _)"  [51, 51] 50)

-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
-
-abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
+notation (input)
+  greater  (infix ">" 50)

notation (input)
+  greater_eq  (infix ">=" 50)
+and
greater_eq  (infix "\<ge>" 50)

syntax```