HOL-Word-Examples
authorhuffman
Tue, 28 Aug 2007 03:56:24 +0200
changeset 24442 39e29972cb96
parent 24441 d2a5295570d0
child 24443 ab6206ccb570
HOL-Word-Examples
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: