# HG changeset patch
# User wenzelm
# Date 1125495995 -7200
# Node ID ffe8efe856e3fe9121b0bb2fef63d72d0eaf6b07
# Parent  917c6e7ca28d416ab69a7ffcb48d5c5ec66951d7
added Complex/ex/BigO_Complex.thy;

diff -r 917c6e7ca28d -r ffe8efe856e3 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Wed Aug 31 15:46:34 2005 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Wed Aug 31 15:46:35 2005 +0200
@@ -11,3 +11,6 @@
 use_thy "Sqrt_Script";
 (*This example also needs the theory Factorization.*)
 use_thy "NSPrimes";
+
+no_document use_thy "BigO";
+use_thy "BigO_Complex";
diff -r 917c6e7ca28d -r ffe8efe856e3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 31 15:46:34 2005 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 31 15:46:35 2005 +0200
@@ -166,8 +166,8 @@
 
 $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
-  Complex/ex/BinEx.thy Complex/ex/NSPrimes.thy\
-  Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
+  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
+  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex