src/HOL/ZF/LProd.thy
changeset 23477 f4b83f03cac9
parent 22282 71b4aefad227
child 23771 bde6db239efa
     1.1 --- a/src/HOL/ZF/LProd.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/ZF/LProd.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -45,9 +45,9 @@
     1.4    case (lprod_list ah at bh bt a b) 
     1.5    from prems have transR: "transP R" by auto
     1.6    have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
     1.7 -    by (simp add: ring_eq_simps)
     1.8 +    by (simp add: ring_simps)
     1.9    have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    1.10 -    by (simp add: ring_eq_simps)
    1.11 +    by (simp add: ring_simps)
    1.12    from prems have "mult R ?ma ?mb"
    1.13      by auto
    1.14    with mult_implies_one_step[OF transR] have 
    1.15 @@ -66,7 +66,7 @@
    1.16      then show ?thesis
    1.17        apply (simp only: as bs)
    1.18        apply (simp only: decomposed True)
    1.19 -      apply (simp add: ring_eq_simps)
    1.20 +      apply (simp add: ring_simps)
    1.21        done
    1.22    next
    1.23      case False
    1.24 @@ -78,7 +78,7 @@
    1.25      then show ?thesis
    1.26        apply (simp only: as bs)
    1.27        apply (simp only: decomposed)
    1.28 -      apply (simp add: ring_eq_simps)
    1.29 +      apply (simp add: ring_simps)
    1.30        done
    1.31    qed
    1.32  qed