src/HOL/Orderings.thy
changeset 23182 01fa88b79ddc
parent 23087 ad7244663431
child 23212 82881b1ae9c6
     1.1 --- a/src/HOL/Orderings.thy	Fri Jun 01 10:44:26 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Jun 01 10:44:28 2007 +0200
     1.3 @@ -310,7 +310,6 @@
     1.4  lemmas order_less_asym = order_class.less_asym
     1.5  lemmas order_eq_iff = order_class.eq_iff
     1.6  lemmas order_antisym_conv = order_class.antisym_conv
     1.7 -lemmas less_imp_neq = order_class.less_imp_neq
     1.8  lemmas order_less_trans = order_class.less_trans
     1.9  lemmas order_le_less_trans = order_class.le_less_trans
    1.10  lemmas order_less_le_trans = order_class.less_le_trans
    1.11 @@ -329,9 +328,6 @@
    1.12  lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
    1.13  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    1.14  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    1.15 -lemmas leI = linorder_class.leI
    1.16 -lemmas leD = linorder_class.leD
    1.17 -lemmas not_leE = linorder_class.not_leE
    1.18  
    1.19  lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
    1.20  lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]