src/HOL/NthRoot.thy
changeset 58709 efdc6c533bd3
parent 57514 bdc2c6b40bf2
child 58770 ae5e9b4f8daf
     1.1 --- a/src/HOL/NthRoot.thy	Sun Oct 19 12:47:34 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Sun Oct 19 18:05:26 2014 +0200
     1.3 @@ -429,8 +429,7 @@
     1.4    assumes n: "even n"
     1.5    shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
     1.6  proof -
     1.7 -  from n obtain m where m: "n = 2 * m"
     1.8 -    unfolding even_mult_two_ex ..
     1.9 +  from n obtain m where m: "n = 2 * m" ..
    1.10    from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    1.11      by (simp only: power_mult[symmetric] mult.commute)
    1.12    then show ?thesis