--- a/src/HOL/IsaMakefile Mon Aug 20 00:22:18 2007 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 20 04:34:31 2007 +0200
@@ -6,7 +6,8 @@
default: HOL
generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
-images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal TLA HOL4
+images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
+ HOL-Word TLA HOL4
#Note: keep targets sorted (except for HOL-Library)
test: \
@@ -804,6 +805,30 @@
@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
+## HOL-Word
+
+HOL-Word: HOL $(OUT)/HOL-Word
+
+$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
+ Library/Infinite_Set.thy Library/Parity.thy \
+ Library/Boolean_Algebra.thy Library/Numeral_Type.thy \
+ Word/Num_Lemmas.thy \
+ Word/TdThs.thy \
+ Word/Size.thy \
+ Word/BinGeneral.thy \
+ Word/BinOperations.thy \
+ Word/BinBoolList.thy \
+ Word/BitSyntax.thy \
+ Word/WordDefinition.thy \
+ Word/WordArith.thy \
+ Word/WordBitwise.thy \
+ Word/WordShift.thy \
+ Word/WordGenLib.thy \
+ Word/WordMain.thy \
+ Word/WordExamples.thy
+ @cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
+
+
## clean
clean: