src/HOL/IsaMakefile
changeset 17198 ffe8efe856e3
parent 17023 7425bf9f0f4b
child 17229 aca2ce40be35
equal deleted inserted replaced
17197:917c6e7ca28d 17198:ffe8efe856e3
   164 
   164 
   165 HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
   165 HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
   166 
   166 
   167 $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
   167 $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
   168   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
   168   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
   169   Complex/ex/BinEx.thy Complex/ex/NSPrimes.thy\
   169   Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
   170   Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
   170   Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
   171 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
   171 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
   172 
   172 
   173 
   173 
   174 ## HOL-Library
   174 ## HOL-Library
   175 
   175