src/HOL/Set_Interval.thy

 
 lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
   by (subst sum_subtractf_nat) auto
 
 
-context semiring_parity
+context unique_euclidean_semiring_with_nat
 begin
 
 lemma take_bit_sum:
   "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k a))))"
   for n :: nat

     by (simp add: algebra_simps double_gauss_sum left_add_twice)
 qed
 
 end
 
-context semiring_parity
+context unique_euclidean_semiring_with_nat
 begin
 
 lemma gauss_sum:
   "(\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
   using double_gauss_sum [of n, symmetric] by simp