--- 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)"