added Complex/ex/BigO_Complex.thy;
authorwenzelm
Wed Aug 31 15:46:35 2005 +0200 (2005-08-31)
changeset 17198ffe8efe856e3
parent 17197 917c6e7ca28d
child 17199 59c1bfc81d91
added Complex/ex/BigO_Complex.thy;
src/HOL/Complex/ex/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Complex/ex/ROOT.ML	Wed Aug 31 15:46:34 2005 +0200
     1.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Wed Aug 31 15:46:35 2005 +0200
     1.3 @@ -11,3 +11,6 @@
     1.4  use_thy "Sqrt_Script";
     1.5  (*This example also needs the theory Factorization.*)
     1.6  use_thy "NSPrimes";
     1.7 +
     1.8 +no_document use_thy "BigO";
     1.9 +use_thy "BigO_Complex";
     2.1 --- a/src/HOL/IsaMakefile	Wed Aug 31 15:46:34 2005 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Aug 31 15:46:35 2005 +0200
     2.3 @@ -166,8 +166,8 @@
     2.4  
     2.5  $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
     2.6    Complex/ex/ROOT.ML Complex/ex/document/root.tex \
     2.7 -  Complex/ex/BinEx.thy Complex/ex/NSPrimes.thy\
     2.8 -  Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
     2.9 +  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
    2.10 +  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
    2.11  	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
    2.12  
    2.13