src/HOL/IsaMakefile
changeset 14531 716c9def5614
parent 14516 a183dec876ab
child 14551 2cb6ff394bfb
equal deleted inserted replaced
14530:e94fd774ecf5 14531:716c9def5614
   206 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   206 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   207 
   207 
   208 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   208 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   209   Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
   209   Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
   210   Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   210   Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   211   Induct/PropLog.thy Induct/ROOT.ML \
   211   Induct/PropLog.thy Induct/QuoDataType.thy Induct/ROOT.ML \
   212   Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   212   Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   213   Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   213   Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   214   Induct/Tree.thy Induct/document/root.tex
   214   Induct/Tree.thy Induct/document/root.tex
   215 	@$(ISATOOL) usedir $(OUT)/HOL Induct
   215 	@$(ISATOOL) usedir $(OUT)/HOL Induct
   216 
   216