# HG changeset patch
# User huffman
# Date 1188266184 -7200
# Node ID 39e29972cb96d4e1bf76dc3d6a9b41e46611508d
# Parent  d2a5295570d0c4561c625f6dc3f970396b71f853
HOL-Word-Examples

diff -r d2a5295570d0 -r 39e29972cb96 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Aug 28 03:49:18 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 28 03:56:24 2007 +0200
@@ -44,6 +44,7 @@
   HOL-UNITY \
   HOL-Unix \
   HOL-W0 \
+  HOL-Word-Examples \
   HOL-ZF
     # ^ this is the sort position
 
@@ -826,11 +827,20 @@
   Word/WordGenLib.thy \
   Word/WordBoolList.thy \
   Word/WordMain.thy \
-  Word/WordExamples.thy \
   Word/document/root.tex
 	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 
 
+## HOL-Word-Examples
+
+HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
+
+$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word \
+  Word/Examples/ROOT.ML \
+  Word/Examples/WordExamples.thy
+	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
+
+
 ## clean
 
 clean: