Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Limits.thy
changeset 56536 aefb4a8da31f
parent 56371 fb9ae0727548
child 56541 0e3abadbef39 
--- a/src/HOL/Limits.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Limits.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1239,7 +1239,7 @@
 proof (induct n)
   case (Suc n)
   have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
-    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
+    by (simp add: field_simps real_of_nat_Suc x)
   also have "\<dots> \<le> (x + 1)^Suc n"
     using Suc x by (simp add: mult_left_mono)
   finally show ?case .
isabelle