changeset 61609 | 77b453bd616f |
parent 58878 | f962e42e324d |
child 61945 | 1135b8de26c3 |
--- a/src/HOL/NSA/NatStar.thy Tue Nov 03 11:20:21 2015 +0100 +++ b/src/HOL/NSA/NatStar.thy Tue Nov 10 14:18:41 2015 +0000 @@ -115,7 +115,7 @@ @{term real_of_nat} *} lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" -by transfer (simp add: fun_eq_iff real_of_nat_def) +by transfer (simp add: fun_eq_iff) lemma starfun_inverse_real_of_nat_eq: "N \<in> HNatInfinite