src/HOL/Orderings.thy
changeset 23018 1d29bc31b0cb
parent 22997 d4f3b015b50b
child 23032 b6cb6a131511
--- 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)