src/HOL/Hyperreal/Star.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14468 6be497cacab5
     1.1 --- a/src/HOL/Hyperreal/Star.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/Star.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -456,14 +456,15 @@
     1.4     In this theory since hypreal_hrabs proved here. (To Check:) Maybe
     1.5     move both if possible?
     1.6   -------------------------------------------------------------------*)
     1.7 -lemma Infinitesimal_FreeUltrafilterNat_iff2: "(x:Infinitesimal) =
     1.8 +lemma Infinitesimal_FreeUltrafilterNat_iff2:
     1.9 +     "(x:Infinitesimal) =
    1.10        (EX X:Rep_hypreal(x).
    1.11          ALL m. {n. abs(X n) < inverse(real(Suc m))}
    1.12                 : FreeUltrafilterNat)"
    1.13 -apply (rule_tac z = x in eq_Abs_hypreal)
    1.14 +apply (rule eq_Abs_hypreal [of x])
    1.15  apply (auto intro!: bexI lemma_hyprel_refl 
    1.16 -            simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def 
    1.17 -     hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def)
    1.18 +            simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
    1.19 +     hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
    1.20  apply (drule_tac x = n in spec, ultra)
    1.21  done
    1.22