--- a/src/HOL/Library/Function_Growth.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy Fri Jul 22 11:00:43 2016 +0200
@@ -36,8 +36,8 @@
shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
proof -
define q where "q = m - n"
- moreover with assms have "m = q + n" by (simp add: q_def)
- ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
+ with assms have "m = q + n" by (simp add: q_def)
+ with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
qed