src/HOL/IsaMakefile
changeset 17023 7425bf9f0f4b
parent 17011 08f8408853e3
child 17198 ffe8efe856e3
equal deleted inserted replaced
17022:b257300c3a9c 17023:7425bf9f0f4b
   533 ## HOL-Extraction
   533 ## HOL-Extraction
   534 
   534 
   535 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
   535 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
   536 
   536 
   537 $(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
   537 $(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
   538   Extraction/Higman.thy Extraction/ROOT.ML Extraction/QuotRem.thy \
   538   Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
       
   539   Extraction/QuotRem.thy \
   539   Extraction/Warshall.thy Extraction/document/root.tex \
   540   Extraction/Warshall.thy Extraction/document/root.tex \
   540   Extraction/document/root.bib
   541   Extraction/document/root.bib
   541 	@$(ISATOOL) usedir $(OUT)/HOL Extraction
   542 	@$(ISATOOL) usedir $(OUT)/HOL Extraction
   542 
   543 
   543 
   544