--- a/src/HOL/Matrix/SparseMatrix.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Sat Apr 23 13:00:19 2011 +0200
@@ -6,9 +6,8 @@
imports Matrix
begin
-types
- 'a spvec = "(nat * 'a) list"
- 'a spmat = "('a spvec) spvec"
+type_synonym 'a spvec = "(nat * 'a) list"
+type_synonym 'a spmat = "'a spvec spvec"
definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix"
where "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"