src/HOL/Orderings.thy
changeset 23018 1d29bc31b0cb
parent 22997 d4f3b015b50b
child 23032 b6cb6a131511
     1.1 --- a/src/HOL/Orderings.thy	Sat May 19 11:33:21 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat May 19 11:33:22 2007 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  text {* Reverse order *}
     1.5  
     1.6  lemma order_reverse:
     1.7 -  "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
     1.8 +  "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
     1.9    by unfold_locales
    1.10      (simp add: less_le, auto intro: antisym order_trans)
    1.11  
    1.12 @@ -266,7 +266,7 @@
    1.13  text {* Reverse order *}
    1.14  
    1.15  lemma linorder_reverse:
    1.16 -  "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    1.17 +  "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    1.18    by unfold_locales
    1.19      (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    1.20