src/HOL/SupInf.thy
changeset 37887 2ae085b07f2f
parent 37765 26bdfb7b680b
child 44669 8e6cdb9c00a7
     1.1 --- a/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -417,7 +417,7 @@
     1.4    also have "... \<le> e" 
     1.5      apply (rule Sup_asclose) 
     1.6      apply (auto simp add: S)
     1.7 -    apply (metis abs_minus_add_cancel b add_commute diff_def)
     1.8 +    apply (metis abs_minus_add_cancel b add_commute diff_minus)
     1.9      done
    1.10    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
    1.11    thus ?thesis