1.1 --- a/src/HOL/Complex/CLim.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Complex/CLim.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  by (simp add: numeral_2_eq_2)
     1.5  
     1.6  text{*Changing the quantified variable. Install earlier?*}
     1.7 -lemma all_shift: "(\<forall>x::'a::ring. P x) = (\<forall>x. P (x-a))";
     1.8 +lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
     1.9  apply auto 
    1.10  apply (drule_tac x="x+a" in spec) 
    1.11  apply (simp add: diff_minus add_assoc)