src/HOL/Matrix_LP/SparseMatrix.thy
changeset 47108 2a1953f0d20d
parent 46988 9f492f5b0cec
child 47455 26315a545e26
     1.1 --- a/src/HOL/Matrix_LP/SparseMatrix.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -1029,9 +1029,7 @@
     1.4    sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat
     1.5    sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat
     1.6  
     1.7 -lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
     1.8 -
     1.9 -lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] = 
    1.10 +lemmas sparse_row_matrix_arith_simps = 
    1.11    mult_spmat.simps mult_spvec_spmat.simps 
    1.12    addmult_spvec.simps 
    1.13    smult_spvec_empty smult_spvec_cons