src/HOL/IsaMakefile
changeset 11641 0c248bed5225
parent 11609 3f3d1add4d94
child 11659 a68f930bafb2
equal deleted inserted replaced
11640:be1bc3b88480 11641:0c248bed5225
   207 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   207 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   208 
   208 
   209 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   209 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   210   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   210   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   211   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   211   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   212   Induct/LList.ML Induct/LList.thy Induct/Mutil.thy \
   212   Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   213   Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   213   Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   214   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   214   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   215   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   215   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   216   Induct/Tree.thy Induct/document/root.tex
   216   Induct/Tree.thy Induct/document/root.tex
   217 	@$(ISATOOL) usedir $(OUT)/HOL Induct
   217 	@$(ISATOOL) usedir $(OUT)/HOL Induct