src/HOL/SetInterval.ML
changeset 9310 ab706fdb0842
parent 8956 a7c3538fc2d2
child 13596 ee5f79b210c1
     1.1 --- a/src/HOL/SetInterval.ML	Thu Jul 13 23:08:42 2000 +0200
     1.2 +++ b/src/HOL/SetInterval.ML	Thu Jul 13 23:09:03 2000 +0200
     1.3 @@ -132,21 +132,9 @@
     1.4  by (Blast_tac 1);
     1.5  qed "UN_atMost_UNIV";
     1.6  
     1.7 -Goalw [atMost_def, le_def]
     1.8 -    "!!k:: 'a::linorder. -atMost k = greaterThan k";
     1.9 -by Auto_tac;
    1.10 -by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    1.11 -by (blast_tac (claset() addIs [order_le_less_trans RS 
    1.12 -	                       (order_less_irrefl RS notE)]) 1);
    1.13 -qed "Compl_atMost";
    1.14 -Addsimps [Compl_atMost];
    1.15 -
    1.16  
    1.17  (*** Combined properties ***)
    1.18  
    1.19  Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
    1.20  by (blast_tac (claset() addIs [order_antisym]) 1);
    1.21  qed "atMost_Int_atLeast";
    1.22 -
    1.23 -
    1.24 -