--- a/src/HOL/ZF/LProd.thy Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/ZF/LProd.thy Wed Jan 28 16:29:16 2009 +0100
@@ -45,9 +45,9 @@
case (lprod_list ah at bh bt a b)
from prems have transR: "trans R" by auto
have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
from prems have "(?ma, ?mb) \<in> mult R"
by auto
with mult_implies_one_step[OF transR] have
@@ -66,7 +66,7 @@
then show ?thesis
apply (simp only: as bs)
apply (simp only: decomposed True)
- apply (simp add: ring_simps)
+ apply (simp add: algebra_simps)
done
next
case False
@@ -78,7 +78,7 @@
then show ?thesis
apply (simp only: as bs)
apply (simp only: decomposed)
- apply (simp add: ring_simps)
+ apply (simp add: algebra_simps)
done
qed
qed