src/HOL/IsaMakefile
changeset 35249 7024a8a8f36a
parent 35222 4f1fba00f66d
child 35292 e4a431b6d9b7
child 35301 90e42f9ba4d1
child 35319 4140f31b2ed2
child 35328 e8888458dce3
equal deleted inserted replaced
35248:e64950874224 35249:7024a8a8f36a
   453 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   453 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
   454 
   454 
   455 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
   455 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
   456   Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
   456   Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
   457   Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
   457   Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
   458   Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/Term.thy		\
   458   Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy		\
   459   Induct/Tree.thy Induct/document/root.tex
   459   Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
   460 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
   460 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
   461 
   461 
   462 
   462 
   463 ## HOL-IMP
   463 ## HOL-IMP
   464 
   464