src/HOL/IsaMakefile
changeset 47602 3d44790b5ab0
parent 47567 407cabf66f21
child 47613 e72e44cee6f2
--- a/src/HOL/IsaMakefile	Thu Apr 19 12:28:10 2012 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 19 17:32:30 2012 +0200
@@ -525,9 +525,12 @@
 HOL-IMP: HOL $(OUT)/HOL-IMP
 
 $(OUT)/HOL-IMP: $(OUT)/HOL \
-  IMP/ACom.thy IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \
-  IMP/Abs_Int0_const.thy IMP/Abs_Int1.thy IMP/Abs_Int1_ivl.thy \
-  IMP/Abs_Int2.thy IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
+  IMP/ACom.thy \
+  IMP/Abs_Int_ITP/Abs_Int0_ITP.thy IMP/Abs_Int_ITP/Abs_State_ITP.thy \
+  IMP/Abs_Int_ITP/Abs_Int1_ITP.thy IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy \
+  IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy IMP/Abs_Int_ITP/Abs_Int2_ITP.thy \
+  IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy IMP/Abs_Int_ITP/Abs_Int3_ITP.thy \
+  IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
   IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \
   IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
   IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \