# HG changeset patch # User wenzelm # Date 1361819502 -3600 # Node ID aba03f0c62548f499397ddc684420f2871dea8c3 # Parent 31e786e0e6a74728db20afb89e07a909f768f53e fixed document; diff -r 31e786e0e6a7 -r aba03f0c6254 src/HOL/Library/Function_Growth.thy --- 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 (\O-Notation\). 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 \ 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 \ o(g) \ f \ g"} is provable, and this yields a handy introduction rule. - Note that D. Knuth ignores @{text o} altogether. So what\ + 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 "(\)"}. In the typical definition of @{text o}, @@ -291,10 +291,10 @@ text {* @{prop "(\n. Suc k * f n) \ f"} *} lemma "f \ (\n. f n + g n)" -by rule auto + by rule auto lemma "(\_. 0) \ (\n. Suc k)" -by (rule less_fun_strongI) auto + by (rule less_fun_strongI) auto lemma "(\_. k) \ Discrete.log" proof (rule less_fun_strongI) @@ -335,10 +335,10 @@ qed lemma "id \ (\n. n\)" -by (rule less_fun_strongI) (auto simp add: power2_eq_square) + by (rule less_fun_strongI) (auto simp add: power2_eq_square) lemma "(\n. n ^ k) \ (\n. n ^ Suc k)" -by (rule less_fun_strongI) auto + by (rule less_fun_strongI) auto text {* @{prop "(\n. n ^ k) \ (\n. 2 ^ n)"} *}