# 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