--- a/src/HOL/IsaMakefile Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IsaMakefile Mon Jun 06 16:29:38 2011 +0200
@@ -527,8 +527,16 @@
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
- IMP/Big_Step.thy IMP/Com.thy IMP/Compiler.thy IMP/Denotation.thy \
- IMP/Poly_Types.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
+ IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.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 \
+ IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \
+ IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \
+ IMP/Live.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \
+ IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
+ IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
+ 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