--- a/src/HOL/Matrix_LP/ComputeNumeral.thy Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy Tue Nov 17 12:32:08 2015 +0000
@@ -28,11 +28,11 @@
lemmas compute_natarith =
arith_simps rel_simps
diff_nat_numeral nat_numeral nat_0 nat_neg_numeral
- numeral_1_eq_1 [symmetric]
+ numeral_One [symmetric]
numeral_1_eq_Suc_0 [symmetric]
Suc_numeral natfac.simps
-lemmas number_norm = numeral_1_eq_1[symmetric]
+lemmas number_norm = numeral_One[symmetric]
lemmas compute_numberarith =
arith_simps rel_simps number_norm