diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Fri Feb 05 21:12:45 1999 +0100
+++ b/src/Sequents/IsaMakefile	Fri Feb 05 21:14:17 1999 +0100
@@ -8,7 +8,7 @@
 
 default: Sequents
 images: Sequents
-test: Sequents-ex
+test: Sequents-ILL Sequents-LK Sequents-Modal
 all: images test
 
 
@@ -31,19 +31,36 @@
 	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
 
 
-## Sequents-ex
+## Sequents-ILL
+
+Sequents-ILL: Sequents $(LOG)/Sequents-ILL.gz
 
-Sequents-ex: Sequents $(LOG)/Sequents-ex.gz
+$(LOG)/Sequents-ILL.gz: $(OUT)/Sequents ILL/ILL_kleene_lemmas.ML \
+  ILL/ILL_predlog.ML ILL/ILL_predlog.thy ILL/ROOT.ML ILL/washing.ML \
+  ILL/washing.thy
+	@$(ISATOOL) usedir $(OUT)/Sequents ILL
+
+
+## Sequents-LK
 
-$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \
-  ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \
-  ex/ILL/washing.thy ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML \
-  ex/LK/quant.ML ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML \
-  ex/Modal/Tthms.ML ex/ROOT.ML
-	@$(ISATOOL) usedir $(OUT)/Sequents ex
+Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
+
+$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
+  LK/prop.ML LK/quant.ML
+	@$(ISATOOL) usedir $(OUT)/Sequents LK
+
+
+## Sequents-Modal
+
+Sequents-Modal: Sequents $(LOG)/Sequents-Modal.gz
+
+$(LOG)/Sequents-Modal.gz: $(OUT)/Sequents Modal/ROOT.ML \
+  Modal/S43thms.ML Modal/S4thms.ML Modal/Tthms.ML ROOT.ML
+	@$(ISATOOL) usedir $(OUT)/Sequents Modal
 
 
 ## clean
 
 clean:
-	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz
+	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ILL.gz \
+	  $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz