src/HOL/Orderings.thy
changeset 36635 080b755377c0
parent 35828 46cfc4b8112e
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Orderings.thy	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  text {* Dual order *}
     1.5  
     1.6  lemma dual_preorder:
     1.7 -  "preorder (op \<ge>) (op >)"
     1.8 +  "class.preorder (op \<ge>) (op >)"
     1.9  proof qed (auto simp add: less_le_not_le intro: order_trans)
    1.10  
    1.11  end
    1.12 @@ -186,7 +186,7 @@
    1.13  text {* Dual order *}
    1.14  
    1.15  lemma dual_order:
    1.16 -  "order (op \<ge>) (op >)"
    1.17 +  "class.order (op \<ge>) (op >)"
    1.18  by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
    1.19  
    1.20  end
    1.21 @@ -257,8 +257,8 @@
    1.22  text {* Dual order *}
    1.23  
    1.24  lemma dual_linorder:
    1.25 -  "linorder (op \<ge>) (op >)"
    1.26 -by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
    1.27 +  "class.linorder (op \<ge>) (op >)"
    1.28 +by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
    1.29  
    1.30  
    1.31  text {* min/max *}