--- 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";
-
-
-