src/HOL/IsaMakefile
changeset 28825 415c7ffeb4cb
parent 28798 a0dd52dd7b55
child 28905 c999579a5166
equal deleted inserted replaced
28824:1db25e5703e3 28825:415c7ffeb4cb
   352 
   352 
   353 ## HOL-Induct
   353 ## HOL-Induct
   354 
   354 
   355 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   355 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   356 
   356 
   357 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
   357 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy	\
   358   Induct/LFilter.thy Induct/LList.thy Induct/Mutil.thy			\
   358   Induct/LFilter.thy Induct/LList.thy Induct/Ordinals.thy	\
   359   Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
   359   Induct/PropLog.thy Induct/QuoNestedDataType.thy		\
   360   Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
   360   Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy		\
   361   Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy		\
   361   Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy	\
   362   Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
   362   Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
   363 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
   363 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
   364 
   364 
   365 
   365 
   366 ## HOL-IMP
   366 ## HOL-IMP