src/HOL/Library/Landau_Symbols.thy

--- a/src/HOL/Library/Landau_Symbols.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -26,38 +26,38 @@
 \<close>
 
 definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
-    ("(1O[_]'(_'))")
+    (\<open>(1O[_]'(_'))\<close>)
   where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"  
 
 definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
-    ("(1o[_]'(_'))")
+    (\<open>(1o[_]'(_'))\<close>)
   where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
 
 definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
-    ("(1\<Omega>[_]'(_'))")
+    (\<open>(1\<Omega>[_]'(_'))\<close>)
   where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"  
 
 definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
-    ("(1\<omega>[_]'(_'))")
+    (\<open>(1\<omega>[_]'(_'))\<close>)
   where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
 
 definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
-    ("(1\<Theta>[_]'(_'))")
+    (\<open>(1\<Theta>[_]'(_'))\<close>)
   where "bigtheta F g = bigo F g \<inter> bigomega F g"
 
-abbreviation bigo_at_top ("(2O'(_'))") where
+abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where
   "O(g) \<equiv> bigo at_top g"    
 
-abbreviation smallo_at_top ("(2o'(_'))") where
+abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where
   "o(g) \<equiv> smallo at_top g"
 
-abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
+abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where
   "\<Omega>(g) \<equiv> bigomega at_top g"
 
-abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
+abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where
   "\<omega>(g) \<equiv> smallomega at_top g"
 
-abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
+abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where
   "\<Theta>(g) \<equiv> bigtheta at_top g"
     
 
@@ -1649,7 +1649,7 @@
 named_theorems asymp_equiv_simps
 
 definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  ("_ \<sim>[_] _" [51, 10, 51] 50)
+  (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)
   where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
 
 abbreviation (input) asymp_equiv_at_top where
@@ -1657,7 +1657,7 @@
 
 bundle asymp_equiv_notation
 begin
-notation asymp_equiv_at_top (infix "\<sim>" 50) 
+notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50) 
 end
 
 lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"