# HG changeset patch
# User wenzelm
# Date 963522543 -7200
# Node ID ab706fdb0842c848baab82c188e23b7a0c0fc4d9
# Parent  4078d5e8b29393315fb11706fdd2dc4032bf9f0e
removed duplicate Compl_atMost;

diff -r 4078d5e8b293 -r ab706fdb0842 src/HOL/SetInterval.ML
--- a/src/HOL/SetInterval.ML	Thu Jul 13 23:08:42 2000 +0200
+++ b/src/HOL/SetInterval.ML	Thu Jul 13 23:09:03 2000 +0200
@@ -132,21 +132,9 @@
 by (Blast_tac 1);
 qed "UN_atMost_UNIV";
 
-Goalw [atMost_def, le_def]
-    "!!k:: 'a::linorder. -atMost k = greaterThan k";
-by Auto_tac;
-by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
-by (blast_tac (claset() addIs [order_le_less_trans RS 
-	                       (order_less_irrefl RS notE)]) 1);
-qed "Compl_atMost";
-Addsimps [Compl_atMost];
-
 
 (*** Combined properties ***)
 
 Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
 by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "atMost_Int_atLeast";
-
-
-