# HG changeset patch
# User haftmann
# Date 1273559382 -7200
# Node ID 354b15d5b4ca7599ff900a4e787518bda6fb64d3
# Parent  cbeb3484fa077c56f70d1819f0f06c163e89e6bc
tuned

diff -r cbeb3484fa07 -r 354b15d5b4ca src/HOL/ex/Landau.thy
--- a/src/HOL/ex/Landau.thy	Tue May 11 08:29:42 2010 +0200
+++ b/src/HOL/ex/Landau.thy	Tue May 11 08:29:42 2010 +0200
@@ -8,8 +8,8 @@
 begin
 
 text {*
-  We establish a preorder releation @{text "\<lesssim>"} on functions
-  from @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
+  We establish a preorder releation @{text "\<lesssim>"} on functions from
+  @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
 *}
 
 subsection {* Auxiliary *}
@@ -175,12 +175,12 @@
 
 text {*
   We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
-  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not manage to
-  do so.
+  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not
+  manage to do so.
 *}
 
 
-subsection {* Assert that @{text "\<lesssim>"} is ineed a preorder *}
+subsection {* Assert that @{text "\<lesssim>"} is indeed a preorder *}
 
 interpretation fun_order: preorder_equiv less_eq_fun less_fun
   where "preorder_equiv.equiv less_eq_fun = equiv_fun"