diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 24 18:32:53 2007 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 24 18:36:09 2007 +0200
@@ -37,6 +37,7 @@
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-SET-Protocol \
+  HOL-Statespace \
   HOL-Subst \
       TLA-Buffer \
       TLA-Inc \
@@ -845,6 +846,17 @@
   Word/Examples/WordExamples.thy
 	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
 
+## HOL-Statespace
+
+HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
+
+$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
+  Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
+  Statespace/StateSpaceSyntax.thy StateSpace/StateSpaceEx.thy \
+  Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
+  Statespace/state_fun.ML \
+  Statespace/document/root.tex
+	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
 
 ## clean