src/HOL/NSA/CLim.thy
changeset 58860 fee7cfa69c50
parent 57514 bdc2c6b40bf2
child 58878 f962e42e324d
     1.1 --- a/src/HOL/NSA/CLim.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/NSA/CLim.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -19,7 +19,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::comm_ring_1. 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: add.assoc)