src/HOL/IsaMakefile
changeset 11850 cdfc3fce577e
parent 11837 b2a9853ec6dd
child 12020 a24373086908
equal deleted inserted replaced
11849:53e629437bc8 11850:cdfc3fce577e
   170   Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
   170   Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
   171   Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
   171   Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
   172   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
   172   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
   173   Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
   173   Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
   174   Real/HahnBanach/document/root.tex
   174   Real/HahnBanach/document/root.tex
   175 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
   175 	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Real HahnBanach
   176 
   176 
   177 
   177 
   178 ## HOL-Library
   178 ## HOL-Library
   179 
   179 
   180 HOL-Library: HOL $(LOG)/HOL-Library.gz
   180 HOL-Library: HOL $(LOG)/HOL-Library.gz
   246   NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
   246   NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
   247   NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
   247   NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
   248   NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
   248   NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
   249   NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
   249   NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
   250   NumberTheory/ROOT.ML
   250   NumberTheory/ROOT.ML
   251 	@$(ISATOOL) usedir $(OUT)/HOL NumberTheory
   251 	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
   252 
   252 
   253 
   253 
   254 ## HOL-GroupTheory
   254 ## HOL-GroupTheory
   255 
   255 
   256 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
   256 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
   409 
   409 
   410 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   410 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   411   Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
   411   Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
   412   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
   412   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
   413   Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML Lambda/document/root.tex
   413   Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML Lambda/document/root.tex
   414 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
   414 	@$(ISATOOL) usedir -g true $(OUT)/HOL Lambda
   415 
   415 
   416 
   416 
   417 ## HOL-Prolog
   417 ## HOL-Prolog
   418 
   418 
   419 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
   419 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
   464   MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \
   464   MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \
   465   MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
   465   MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
   466   MicroJava/BV/Step.thy MicroJava/BV/StepMono.thy \
   466   MicroJava/BV/Step.thy MicroJava/BV/StepMono.thy \
   467   MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
   467   MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
   468   MicroJava/document/root.bib MicroJava/document/root.tex
   468   MicroJava/document/root.bib MicroJava/document/root.tex
   469 	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
   469 	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
       
   470 
   470 
   471 
   471 ## HOL-NanoJava
   472 ## HOL-NanoJava
   472 
   473 
   473 HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
   474 HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
   474 
   475 
   475 $(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
   476 $(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
   476   NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
   477   NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
   477   NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
   478   NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
   478   NanoJava/document/root.bib NanoJava/document/root.tex
   479   NanoJava/document/root.bib NanoJava/document/root.tex
   479 	@$(ISATOOL) usedir $(OUT)/HOL NanoJava
   480 	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
       
   481 
   480 
   482 
   481 ## HOL-CTL
   483 ## HOL-CTL
   482 
   484 
   483 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
   485 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
   484 
   486