--- a/src/HOL/Orderings.thy Wed Jan 30 10:57:44 2008 +0100
+++ b/src/HOL/Orderings.thy Wed Jan 30 10:57:46 2008 +0100
@@ -106,9 +106,9 @@
by (rule less_asym)
-text {* Reverse order *}
+text {* Dual order *}
-lemma order_reverse:
+lemma dual_order:
"order (op \<ge>) (op >)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans)
@@ -179,9 +179,9 @@
unfolding not_le .
-text {* Reverse order *}
+text {* Dual order *}
-lemma linorder_reverse:
+lemma dual_linorder:
"linorder (op \<ge>) (op >)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans simp add: linear)