# HG changeset patch
# User wenzelm
# Date 1515773674 -3600
# Node ID 060efe5321898ae789b0fb9e699beab037d25bec
# Parent  4a4c14b2480084ad4f0da12450548822d67030b9
prefer formal text;

diff -r 4a4c14b24800 -r 060efe532189 src/HOL/Library/Going_To_Filter.thy
--- a/src/HOL/Library/Going_To_Filter.thy	Fri Jan 12 15:27:46 2018 +0100
+++ b/src/HOL/Library/Going_To_Filter.thy	Fri Jan 12 17:14:34 2018 +0100
@@ -4,7 +4,9 @@
 
   A filter describing the points x such that f(x) tends to some other filter.
 *)
-section \<open>The `going\_to' filter\<close>
+
+section \<open>The \<open>going_to\<close> filter\<close>
+
 theory Going_To_Filter
   imports Complex_Main
 begin
@@ -18,7 +20,7 @@
     where "f going_to F \<equiv> f going_to F within UNIV"
 
 text \<open>
-  The `going\_to' filter is, in a sense, the opposite of @{term filtermap}. 
+  The \<open>going_to\<close> filter is, in a sense, the opposite of @{term filtermap}. 
   It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the 
   range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be 
   written as @{term "f going_to F"}.
@@ -27,7 +29,7 @@
   of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
   as @{term "norm going_to at_top"}.
 
-  Additionally, the `going\_to' filter can be restricted with an optional `within' parameter.
+  Additionally, the \<open>going_to\<close> filter can be restricted with an optional `within' parameter.
   For instance, if one would would want to consider the filter of complex numbers near infinity
   that do not lie on the negative real line, one could write 
   @{term "norm going_to at_top within - complex_of_real ` {..0}"}.