src/HOL/SupInf.thy
changeset 35823 bd26885af9f4
parent 35581 a25e51e2d64d
child 36007 095b1022e2ae
     1.1 --- a/src/HOL/SupInf.thy	Thu Mar 18 13:56:34 2010 +0100
     1.2 +++ b/src/HOL/SupInf.thy	Thu Mar 18 13:56:34 2010 +0100
     1.3 @@ -355,13 +355,13 @@
     1.4  
     1.5  lemma Inf_greater:
     1.6    fixes z :: real
     1.7 -  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
     1.8 +  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
     1.9    by (metis Inf_real_iff mem_def not_leE)
    1.10  
    1.11  lemma Inf_close:
    1.12    fixes e :: real
    1.13    shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
    1.14 -  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
    1.15 +  by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
    1.16  
    1.17  lemma Inf_finite_Min:
    1.18    fixes S :: "real set"
    1.19 @@ -417,7 +417,7 @@
    1.20    also have "... \<le> e" 
    1.21      apply (rule Sup_asclose) 
    1.22      apply (auto simp add: S)
    1.23 -    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
    1.24 +    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
    1.25      done
    1.26    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
    1.27    thus ?thesis