src/HOL/ex/Function_Growth.thy

   "f \<cong> g \<longleftrightarrow>
     (\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)"
 
 text \<open>
   This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
-  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
+  restricted to \<^typ>\<open>nat\<close>, see note above on \<open>(\<lesssim>)\<close>.
 \<close>
 
 lemma equiv_funI:
   assumes "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   shows "f \<cong> g"

   Something still has to be said about the coefficient \<open>c\<close> in
   the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
   it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
   is that the situation is dual to the definition of \<open>O\<close>: the definition
   works since \<open>c\<close> may become arbitrary small.  Since this is not possible
-  within @{term \<nat>}, we push the coefficient to the left hand side instead such
+  within \<^term>\<open>\<nat>\<close>, we push the coefficient to the left hand side instead such
   that it may become arbitrary big instead.
 \<close>
 
 lemma less_fun_strongI:
   assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"

   preconditions to the functions may be necessary.  The list here is by no means to be
   intended as complete construction set for typical functions, here surely something
   has to be added yet.
 \<close>
 
-text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
+text \<open>\<^prop>\<open>(\<lambda>n. f n + k) \<cong> f\<close>\<close>
 
 lemma equiv_fun_mono_const:
   assumes "mono f" and "\<exists>n. f n > 0"
   shows "(\<lambda>n. f n + k) \<cong> f"
 proof (cases "k = 0")

 qed
 
 (*lemma
   "Discrete.log \<prec> Discrete.sqrt"
 proof (rule less_fun_strongI)*)
-text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
+text \<open>\<^prop>\<open>Discrete.log \<prec> Discrete.sqrt\<close>\<close>
 
 lemma
   "Discrete.sqrt \<prec> id"
 proof (rule less_fun_strongI)
   fix c :: nat

   by (rule less_fun_strongI) auto
 
 (*lemma 
   "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
 proof (rule less_fun_strongI)*)
-text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
+text \<open>\<^prop>\<open>(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)\<close>\<close>
 
 end