src/HOL/Power.thy
changeset 63040 eb4ddd18d635
parent 62481 b5d8e57826df
child 63417 c184ec919c70
     1.1 --- a/src/HOL/Power.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4    case 0 then show ?case by (simp add: fun_eq_iff)
     1.5  next
     1.6    case (Suc n)
     1.7 -  def g \<equiv> "\<lambda>x. f x - 1"
     1.8 +  define g where "g x = f x - 1" for x
     1.9    with Suc have "n = g x" by simp
    1.10    with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    1.11    moreover from Suc g_def have "f x = g x + 1" by simp