src/HOL/Orderings.thy
changeset 25103 1ee419a5a30f
parent 25076 a50b36401c61
child 25193 e2e1a4b00de3
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 19 19:45:29 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 19 19:45:31 2007 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  text {* Reverse order *}
     1.5  
     1.6  lemma order_reverse:
     1.7 -  "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
     1.8 +  "order (op \<ge>) (op >)"
     1.9  by unfold_locales
    1.10     (simp add: less_le, auto intro: antisym order_trans)
    1.11  
    1.12 @@ -187,7 +187,7 @@
    1.13  text {* Reverse order *}
    1.14  
    1.15  lemma linorder_reverse:
    1.16 -  "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
    1.17 +  "linorder (op \<ge>) (op >)"
    1.18  by unfold_locales
    1.19    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    1.20  
    1.21 @@ -597,15 +597,6 @@
    1.22  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    1.23  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    1.24  
    1.25 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
    1.26 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
    1.27 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
    1.28 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
    1.29 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
    1.30 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
    1.31 -lemmas split_min = linorder_class.split_min
    1.32 -lemmas split_max = linorder_class.split_max
    1.33 -
    1.34  
    1.35  subsection {* Bounded quantifiers *}
    1.36