--- a/src/HOL/Orderings.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Orderings.thy Tue May 04 08:55:43 2010 +0200
@@ -106,7 +106,7 @@
text {* Dual order *}
lemma dual_preorder:
- "preorder (op \<ge>) (op >)"
+ "class.preorder (op \<ge>) (op >)"
proof qed (auto simp add: less_le_not_le intro: order_trans)
end
@@ -186,7 +186,7 @@
text {* Dual order *}
lemma dual_order:
- "order (op \<ge>) (op >)"
+ "class.order (op \<ge>) (op >)"
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
end
@@ -257,8 +257,8 @@
text {* Dual order *}
lemma dual_linorder:
- "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+ "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
text {* min/max *}