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/Free_Ultrafilter.thy
changeset 69597 ff784d5a5bfb
parent 68745 345ce5f262ea 
--- a/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -49,7 +49,7 @@
 
 text \<open>
    A filter \<open>F\<close> is an ultrafilter iff it is a maximal filter,
-   i.e. whenever \<open>G\<close> is a filter and @{prop "F \<subseteq> G"} then @{prop "F = G"}
+   i.e. whenever \<open>G\<close> is a filter and \<^prop>\<open>F \<subseteq> G\<close> then \<^prop>\<open>F = G\<close>
 \<close>
 
 text \<open>
isabelle