--- a/src/HOL/Orderings.thy Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Orderings.thy Sat May 19 11:33:22 2007 +0200
@@ -199,7 +199,7 @@
text {* Reverse order *}
lemma order_reverse:
- "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans)
@@ -266,7 +266,7 @@
text {* Reverse order *}
lemma linorder_reverse:
- "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans simp add: linear)