diff -r 2230b7047376 -r 9a5f43dac883 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -155,8 +155,8 @@
 
 lemma not_true_eq_false: "(~ True) = False" by simp
 
-lemmas powerarith = nat_numeral zpower_numeral_even
-  zpower_numeral_odd zpower_Pls
+lemmas powerarith = nat_numeral power_numeral_even
+  power_numeral_odd zpower_Pls
 
 definition float :: "(int \<times> int) \<Rightarrow> real" where
   "float = (\<lambda>(a, b). real_of_int a * 2 powr real_of_int b)"