src/HOL/IsaMakefile
changeset 11046 b5f5942781a0
parent 11026 a50365d21144
child 11049 7eef34adb852
equal deleted inserted replaced
11045:971a50fda146 11046:b5f5942781a0
   203 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   203 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   204 
   204 
   205 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   205 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   206   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   206   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   207   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   207   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   208   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
   208   Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \
   209   Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
   209   Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   210   Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
   210   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   211   Induct/Sigma_Algebra.thy Induct/SList.ML Induct/SList.thy \
   211   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   212   Induct/ABexp.ML Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
   212   Induct/Tree.thy Induct/document/root.tex
   213 	@$(ISATOOL) usedir $(OUT)/HOL Induct
   213 	@$(ISATOOL) usedir $(OUT)/HOL Induct
   214 
   214 
   215 
   215 
   216 ## HOL-IMP
   216 ## HOL-IMP
   217 
   217