diff -r c7d69df58482 -r 19e735596e51 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Sep 10 20:04:14 2004 +0200
@@ -188,8 +188,6 @@
   (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
   apply (rule addmult_spvec.induct[of _ y])
   apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
-  apply (case_tac "a=aa")
-  apply (auto)
   done
 
 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
@@ -403,8 +401,6 @@
 lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
   apply (rule add_spvec.induct[of _ a b])
   apply (simp_all add: singleton_matrix_add)
-  apply (case_tac "a = aa")
-  apply (simp_all)
   done
 
 recdef add_spmat "measure (% (A,B). (length A)+(length B))"
@@ -421,7 +417,6 @@
 lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
   apply (rule add_spmat.induct)
   apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
-  apply (case_tac "a=aa", simp, simp)+
   done
 
 lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"