HOLCF-FOCUS depends on ex/Stream.thy
authorhuffman
Thu, 18 Feb 2010 12:36:09 -0800
changeset 35214 67689d276c70
parent 35213 b9866ad4e3be
child 35215 a03462cbf86f
HOLCF-FOCUS depends on ex/Stream.thy
src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Feb 18 08:08:51 2010 -0800
+++ b/src/HOLCF/IsaMakefile	Thu Feb 18 12:36:09 2010 -0800
@@ -113,7 +113,9 @@
 
 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
 
-$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \
+$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
+  ex/Stream.thy \
+  FOCUS/Fstreams.thy \
   FOCUS/Fstream.thy FOCUS/FOCUS.thy \
   FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
   FOCUS/Buffer.thy FOCUS/Buffer_adm.thy