src/HOL/Orderings.thy
changeset 26014 00c2c3525bef
parent 25614 0b8baa94b866
child 26300 03def556e26e
     1.1 --- a/src/HOL/Orderings.thy	Wed Jan 30 10:57:44 2008 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jan 30 10:57:46 2008 +0100
     1.3 @@ -106,9 +106,9 @@
     1.4  by (rule less_asym)
     1.5  
     1.6  
     1.7 -text {* Reverse order *}
     1.8 +text {* Dual order *}
     1.9  
    1.10 -lemma order_reverse:
    1.11 +lemma dual_order:
    1.12    "order (op \<ge>) (op >)"
    1.13  by unfold_locales
    1.14     (simp add: less_le, auto intro: antisym order_trans)
    1.15 @@ -179,9 +179,9 @@
    1.16  unfolding not_le .
    1.17  
    1.18  
    1.19 -text {* Reverse order *}
    1.20 +text {* Dual order *}
    1.21  
    1.22 -lemma linorder_reverse:
    1.23 +lemma dual_linorder:
    1.24    "linorder (op \<ge>) (op >)"
    1.25  by unfold_locales
    1.26    (simp add: less_le, auto intro: antisym order_trans simp add: linear)