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/Transcendental.thy
changeset 63092 a949b2a5f51d
parent 63040 eb4ddd18d635
child 63145 703edebd1d92 
--- a/src/HOL/Transcendental.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Transcendental.thy	Fri May 13 20:24:10 2016 +0200
@@ -2203,7 +2203,7 @@
 
 lemma powr_mult_base:
   fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
-  using assms by (auto simp: powr_add)
+  by (auto simp: powr_add)
 
 lemma powr_powr:
   fixes x::real shows "(x powr a) powr b = x powr (a * b)"
isabelle