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