--- a/src/HOL/Matrix/cplex/Cplex.thy Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Matrix/cplex/Cplex.thy Wed Jan 28 16:29:16 2009 +0100
@@ -34,8 +34,8 @@
add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
apply (simp add: Let_def)
apply (insert assms)
- apply (simp add: sparse_row_matrix_op_simps ring_simps)
- apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
+ apply (simp add: sparse_row_matrix_op_simps algebra_simps)
+ apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
apply (auto)
done