Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/Star.thy
changeset 20730 da903f59e9ba
parent 20563 44eda2314aab
child 20732 275f9bd2ead9 
--- a/src/HOL/Hyperreal/Star.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -326,7 +326,7 @@
                 \<in>  FreeUltrafilterNat)"
 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
      hnorm_def star_of_nat_def starfun_star_n
-     star_n_inverse star_n_less hypreal_of_nat_eq)
+     star_n_inverse star_n_less real_of_nat_def)
 
 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
       (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
isabelle