changeset 54892 | 64c2d4f8d981 |
parent 47455 | 26315a545e26 |
child 61076 | bdc1e2f0a86a |
--- a/src/HOL/Matrix_LP/SparseMatrix.thy Wed Jan 01 11:35:21 2014 +0100 +++ b/src/HOL/Matrix_LP/SparseMatrix.thy Wed Jan 01 15:55:11 2014 +0100 @@ -240,7 +240,6 @@ fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat \<Rightarrow> 'a spvec" where -(* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *) "mult_spvec_spmat c [] brr = c" | "mult_spvec_spmat c arr [] = c" | "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (