src/HOL/IsaMakefile
changeset 16187 6ec757011ad6
parent 16090 fbb5ae140535
child 16356 94011cf701a4
equal deleted inserted replaced
16186:6eb74e2cec7e 16187:6ec757011ad6
   112   Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
   112   Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
   113   Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
   113   Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
   114   antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
   114   antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
   115   document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML			\
   115   document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML			\
   116   thy_syntax.ML
   116   thy_syntax.ML
   117 	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
   117 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   118 
   118 
   119 
   119 
   120 ## HOL-Complex-HahnBanach
   120 ## HOL-Complex-HahnBanach
   121 
   121 
   122 HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
   122 HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz