src/HOL/IsaMakefile
changeset 29399 ebcd69a00872
parent 29197 6d4cb27ed19c
child 29463 6660f9019673
     1.1 --- a/src/HOL/IsaMakefile	Thu Jan 08 10:53:48 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jan 08 17:10:41 2009 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    HOL-IMP \
     1.5    HOL-IMPP \
     1.6    HOL-IOA \
     1.7 +  HOL-Imperative_HOL \
     1.8    HOL-Induct \
     1.9    HOL-Isar_examples \
    1.10    HOL-Lambda \
    1.11 @@ -325,9 +326,7 @@
    1.12    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
    1.13    Library/Numeral_Type.thy			\
    1.14    Library/Boolean_Algebra.thy Library/Countable.thy	\
    1.15 -  Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
    1.16 -  Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
    1.17 -  Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
    1.18 +  Library/RBT.thy		\
    1.19    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
    1.20  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.21  
    1.22 @@ -625,6 +624,17 @@
    1.23  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
    1.24  
    1.25  
    1.26 +## HOL-Imperative_HOL
    1.27 +
    1.28 +HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
    1.29 +
    1.30 +$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
    1.31 +  Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
    1.32 +  Imperative_HOL/Relational.thy \
    1.33 +  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
    1.34 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    1.35 +
    1.36 +
    1.37  ## HOL-SizeChange
    1.38  
    1.39  HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
    1.40 @@ -796,8 +806,9 @@
    1.41    ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.42    ex/Reflected_Presburger.thy ex/coopertac.ML				\
    1.43    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.44 -  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy			\
    1.45 -  ex/Unification.thy ex/document/root.bib			\
    1.46 +  ex/Subarray.thy ex/Sublist.thy                                        \
    1.47 +  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy	\
    1.48 +  ex/Unification.thy ex/document/root.bib			        \
    1.49    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
    1.50    ex/svc_funcs.ML ex/svc_test.thy	\
    1.51    ex/ImperativeQuicksort.thy	\