src/HOL/IsaMakefile
changeset 43142 2a05c1f7c08c
parent 43124 fdb7e1d5f762
child 43146 09f74fda1b1d
equal deleted inserted replaced
43141:11fce8564415 43142:2a05c1f7c08c
   523 
   523 
   524 ## HOL-IMP
   524 ## HOL-IMP
   525 
   525 
   526 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
   526 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
   527 
   527 
   528 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy		\
   528 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
   529   IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
   529   IMP/Big_Step.thy IMP/Com.thy IMP/Compiler.thy IMP/Denotation.thy 	\
   530   IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
   530   IMP/Small_Step.thy IMP/Star.thy					\
   531   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
   531   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
   532 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
   532 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
   533 
   533 
   534 
   534 
   535 ## HOL-IMPP
   535 ## HOL-IMPP