src/HOL/IsaMakefile
changeset 13129 bb448fb75191
parent 13117 0b233f430076
child 13131 2d284f0dfd56
equal deleted inserted replaced
13128:99f6a9f0328a 13129:bb448fb75191
   231 
   231 
   232 ## HOL-IMP
   232 ## HOL-IMP
   233 
   233 
   234 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
   234 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
   235 
   235 
   236 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy \
   236 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \
   237   IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
   237   IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
   238   IMP/Natural.thy IMP/Examples.thy \
   238   IMP/Natural.thy IMP/Examples.thy \
   239   IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
   239   IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
   240   IMP/document/root.bib
   240   IMP/document/root.bib
   241 	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
   241 	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP