src/HOL/IsaMakefile
changeset 13943 83d842ccd4aa
parent 13939 b3ef90abbd02
child 13949 0ce528cd6f19
equal deleted inserted replaced
13942:dc93e3a68142 13943:83d842ccd4aa
   282 
   282 
   283 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
   283 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
   284 
   284 
   285 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
   285 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
   286   Library/Primes.thy Library/FuncSet.thy \
   286   Library/Primes.thy Library/FuncSet.thy \
   287   GroupTheory/Bij.thy \
       
   288   GroupTheory/Group.thy \
   287   GroupTheory/Group.thy \
   289   GroupTheory/ROOT.ML \
   288   GroupTheory/ROOT.ML \
   290   GroupTheory/document/root.tex
   289   GroupTheory/document/root.tex
   291 	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
   290 	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
   292 
   291 
   339 ## HOL-Algebra
   338 ## HOL-Algebra
   340 
   339 
   341 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
   340 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
   342 
   341 
   343 $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
   342 $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
       
   343   Algebra/Bij.thy \
   344   Algebra/CRing.thy \
   344   Algebra/CRing.thy \
   345   Algebra/Coset.thy \
   345   Algebra/Coset.thy \
   346   Algebra/Exponent.thy \
   346   Algebra/Exponent.thy \
   347   Algebra/FiniteProduct.thy \
   347   Algebra/FiniteProduct.thy \
   348   Algebra/Group.thy \
   348   Algebra/Group.thy \