src/HOL/SEQ.thy
changeset 36776 c137ae7673d3
parent 36663 f75b13ed4898
child 36822 38a480e0346f
     1.1 --- a/src/HOL/SEQ.thy	Sun May 09 09:39:01 2010 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun May 09 14:21:44 2010 -0700
     1.3 @@ -1289,7 +1289,7 @@
     1.4    hence x0: "0 < x" by simp
     1.5    assume x1: "x < 1"
     1.6    from x0 x1 have "1 < inverse x"
     1.7 -    by (rule real_inverse_gt_one)
     1.8 +    by (rule one_less_inverse)
     1.9    hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
    1.10      by (rule LIMSEQ_inverse_realpow_zero)
    1.11    thus ?thesis by (simp add: power_inverse)