src/HOL/NSA/NatStar.thy
changeset 39198 f967a16dfcdd
parent 27468 0783dd1dc13d
child 39302 d7728f65b353
     1.1 --- a/src/HOL/NSA/NatStar.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/NSA/NatStar.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4    @{term real_of_nat} *}
     1.5  
     1.6  lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
     1.7 -by transfer (simp add: expand_fun_eq real_of_nat_def)
     1.8 +by transfer (simp add: ext_iff real_of_nat_def)
     1.9  
    1.10  lemma starfun_inverse_real_of_nat_eq:
    1.11       "N \<in> HNatInfinite