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/Nonstandard_Analysis/NSCA.thy
changeset 67443 3abf6a722518
parent 67091 1393c2340eec
child 67613 ce654b0e6d69 
--- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -14,7 +14,7 @@
    SComplex  :: "hcomplex set" where
    "SComplex \<equiv> Standard"
 
-definition \<comment>\<open>standard part map\<close>
+definition \<comment> \<open>standard part map\<close>
   stc :: "hcomplex => hcomplex" where 
   "stc x = (SOME r. x \<in> HFinite \<and> r\<in>SComplex \<and> r \<approx> x)"
isabelle