--- a/src/HOL/Library/Function_Growth.thy Sun Feb 24 20:29:13 2013 +0100
+++ b/src/HOL/Library/Function_Growth.thy Mon Feb 25 20:11:42 2013 +0100
@@ -11,7 +11,7 @@
text {*
When comparing growth of functions in computer science, it is common to adhere
- on Landau Symbols (\<guillemotright>O-Notation\<guillemotleft>). However these come at the cost of notational
+ on Landau Symbols (``O-Notation''). However these come at the cost of notational
oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
@@ -152,7 +152,7 @@
However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
handy introduction rule.
- Note that D. Knuth ignores @{text o} altogether. So what\<dots>
+ Note that D. Knuth ignores @{text o} altogether. So what \dots
Something still has to be said about the coefficient @{text c} in
the definition of @{text "(\<prec>)"}. In the typical definition of @{text o},
@@ -291,10 +291,10 @@
text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
lemma "f \<lesssim> (\<lambda>n. f n + g n)"
-by rule auto
+ by rule auto
lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
-by (rule less_fun_strongI) auto
+ by (rule less_fun_strongI) auto
lemma "(\<lambda>_. k) \<prec> Discrete.log"
proof (rule less_fun_strongI)
@@ -335,10 +335,10 @@
qed
lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
-by (rule less_fun_strongI) (auto simp add: power2_eq_square)
+ by (rule less_fun_strongI) (auto simp add: power2_eq_square)
lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
-by (rule less_fun_strongI) auto
+ by (rule less_fun_strongI) auto
text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}