# HG changeset patch
# User haftmann
# Date 1180687468 -7200
# Node ID 01fa88b79ddc9cbec1faee5ea780454d4a48eec5
# Parent  f52b555f814168f36ffc5f1e01c6ba783ff7ebaf
dropped superfluous name bindings

diff -r f52b555f8141 -r 01fa88b79ddc src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jun 01 10:44:26 2007 +0200
+++ b/src/HOL/Orderings.thy	Fri Jun 01 10:44:28 2007 +0200
@@ -310,7 +310,6 @@
 lemmas order_less_asym = order_class.less_asym
 lemmas order_eq_iff = order_class.eq_iff
 lemmas order_antisym_conv = order_class.antisym_conv
-lemmas less_imp_neq = order_class.less_imp_neq
 lemmas order_less_trans = order_class.less_trans
 lemmas order_le_less_trans = order_class.le_less_trans
 lemmas order_less_le_trans = order_class.less_le_trans
@@ -329,9 +328,6 @@
 lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
-lemmas leI = linorder_class.leI
-lemmas leD = linorder_class.leD
-lemmas not_leE = linorder_class.not_leE
 
 lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
 lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]