# HG changeset patch # User kleing # Date 1311144377 -7200 # Node ID bce3de79c8ce405a54781b7a207e0b8038fcf1bb # Parent eabe4d6fbd131b2fcc7ad7915e138a0670f20a65 build an image for HOL-IMP diff -r eabe4d6fbd13 -r bce3de79c8ce src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 20 08:16:42 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 20 08:46:17 2011 +0200 @@ -12,6 +12,7 @@ HOL-Library \ HOL-Algebra \ HOL-Boogie \ + HOL-IMP \ HOL-Multivariate_Analysis \ HOL-NSA \ HOL-Nominal \ @@ -39,7 +40,6 @@ HOLCF-Library \ HOLCF-Tutorial \ HOLCF-ex \ - HOL-IMP \ HOL-IMPP \ HOL-IOA \ IOA-ABP \ @@ -526,9 +526,9 @@ ## HOL-IMP -HOL-IMP: HOL $(LOG)/HOL-IMP.gz +HOL-IMP: HOL $(OUT)/HOL-IMP -$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \ +$(OUT)/HOL-IMP: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \ IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \ IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ @@ -540,7 +540,7 @@ IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ IMP/Util.thy IMP/VC.thy IMP/Vars.thy \ IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP + @cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP ## HOL-IMPP @@ -1772,7 +1772,7 @@ $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \ - $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ + $(OUT)/HOL-IMP $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ $(OUT)/HOL-SPARK \