src/HOL/Analysis/Finite_Cartesian_Product.thy

   proof (subst bij_betw_same_card)
     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
       by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
     have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
       (is "_ = card ?A")
-      by (subst card_PiE) (auto simp: prod_constant)
-    
+      by (subst card_PiE) (auto)
     also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
       by auto
     finally show "card \<dots> = CARD('a) ^ CARD('b)" ..
   qed
 qed (simp_all add: infinite_UNIV_vec)

   shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
 
 lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
   apply (vector matrix_vector_mult_def mat_def)
-  apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
+  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
   done
 
 lemma matrix_transpose_mul:
     "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)