src/HOL/Matrix_LP/ComputeNumeral.thy
changeset 61694 6571c78c9667
parent 61609 77b453bd616f
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -28,11 +28,11 @@
     1.4  lemmas compute_natarith =
     1.5    arith_simps rel_simps
     1.6    diff_nat_numeral nat_numeral nat_0 nat_neg_numeral
     1.7 -  numeral_1_eq_1 [symmetric]
     1.8 +  numeral_One [symmetric]
     1.9    numeral_1_eq_Suc_0 [symmetric]
    1.10    Suc_numeral natfac.simps
    1.11  
    1.12 -lemmas number_norm = numeral_1_eq_1[symmetric]
    1.13 +lemmas number_norm = numeral_One[symmetric]
    1.14  
    1.15  lemmas compute_numberarith =
    1.16    arith_simps rel_simps number_norm