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/ExtraThms2.ML
changeset 13810 c3fbfd472365
parent 13153 4b052946b41c 
--- a/src/HOL/Hyperreal/ExtraThms2.ML	Fri Feb 07 15:36:54 2003 +0100
+++ b/src/HOL/Hyperreal/ExtraThms2.ML	Fri Feb 07 16:40:23 2003 +0100
@@ -498,7 +498,7 @@
 Addsimps [HNatInfinite_inverse_not_zero];
 
 Goal "N : HNatInfinite \
-\     ==> (*fNat* (%x. inverse (real x))) N : Infinitesimal";
+\     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
 by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
isabelle