src/HOL/SetInterval.thy
changeset 35216 7641e8d831d2
parent 35171 28f824c7addc
child 35580 0f74806cab22
     1.1 --- a/src/HOL/SetInterval.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -539,7 +539,7 @@
     1.4    apply (rule subset_antisym)
     1.5     apply (rule UN_finite2_subset, blast)
     1.6   apply (rule UN_finite2_subset [where k=k])
     1.7 - apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
     1.8 + apply (force simp add: atLeastLessThan_add_Un [of 0])
     1.9   done
    1.10  
    1.11  
    1.12 @@ -613,7 +613,7 @@
    1.13    apply (unfold image_def lessThan_def)
    1.14    apply auto
    1.15    apply (rule_tac x = "nat x" in exI)
    1.16 -  apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
    1.17 +  apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
    1.18    done
    1.19  
    1.20  lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
    1.21 @@ -1006,7 +1006,7 @@
    1.22    shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
    1.23  proof-
    1.24    have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
    1.25 -  also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
    1.26 +  also have "\<dots> = ?r" by(simp add: mult_commute)
    1.27    finally show ?thesis by auto
    1.28  qed
    1.29  
    1.30 @@ -1046,7 +1046,7 @@
    1.31  lemma geometric_sum:
    1.32    "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
    1.33    (x ^ n - 1) / (x - 1::'a::{field})"
    1.34 -by (induct "n") (simp_all add:field_simps power_Suc)
    1.35 +by (induct "n") (simp_all add: field_simps)
    1.36  
    1.37  subsection {* The formula for arithmetic sums *}
    1.38  
    1.39 @@ -1098,7 +1098,7 @@
    1.40      of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.41      by (rule arith_series_general)
    1.42    thus ?thesis
    1.43 -    unfolding One_nat_def by (auto simp add: of_nat_id)
    1.44 +    unfolding One_nat_def by auto
    1.45  qed
    1.46  
    1.47  lemma arith_series_int: