src/HOL/IsaMakefile

   HOL-HoareParallel \
   HOL-Import \
   HOL-IMP \
   HOL-IMPP \
   HOL-IOA \
+  HOL-Imperative_HOL \
   HOL-Induct \
   HOL-Isar_examples \
   HOL-Lambda \
   HOL-Lattice \
   HOL-Matrix \

   Library/Binomial.thy Library/Eval_Witness.thy	\
   Library/Code_Index.thy Library/Code_Char.thy				\
   Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   Library/Numeral_Type.thy			\
   Library/Boolean_Algebra.thy Library/Countable.thy	\
-  Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
-  Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
-  Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
+  Library/RBT.thy		\
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
 
 ## HOL-HahnBanach

   Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy	\
   Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy	\
   Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy		\
   Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
+
+
+## HOL-Imperative_HOL
+
+HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
+
+$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
+  Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
+  Imperative_HOL/Relational.thy \
+  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
 
 
 ## HOL-SizeChange
 
 HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz

   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
   ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML	\
   ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
   ex/Reflected_Presburger.thy ex/coopertac.ML				\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
-  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy			\
-  ex/Unification.thy ex/document/root.bib			\
+  ex/Subarray.thy ex/Sublist.thy                                        \
+  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy	\
+  ex/Unification.thy ex/document/root.bib			        \
   ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
   ex/svc_funcs.ML ex/svc_test.thy	\
   ex/ImperativeQuicksort.thy	\
   ex/BigO_Complex.thy			\
   ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy	\