# HG changeset patch # User huffman # Date 1158366768 -7200 # Node ID 5a925ad63f4d1549be4e3a943b2144cc50de31df # Parent c643984eb94b3f4d5e2da496cbadd225be7f777b add required type annotation diff -r c643984eb94b -r 5a925ad63f4d src/HOL/Complex/ex/BigO_Complex.thy --- a/src/HOL/Complex/ex/BigO_Complex.thy Fri Sep 15 22:56:17 2006 +0200 +++ b/src/HOL/Complex/ex/BigO_Complex.thy Sat Sep 16 02:32:48 2006 +0200 @@ -13,7 +13,7 @@ Additional lemmas that require the \texttt{HOL-Complex} logic image. *} -lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0" +lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)" apply (simp add: LIMSEQ_def bigo_alt_def) apply clarify apply (drule_tac x = "r / c" in spec) @@ -38,7 +38,7 @@ done lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a - ==> g ----> a" + ==> g ----> (a::real)" apply (drule set_plus_imp_minus) apply (drule bigo_LIMSEQ1) apply assumption