--- a/src/HOL/IsaMakefile Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 03 15:28:24 2001 +0200
@@ -259,8 +259,11 @@
$(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
Library/Primes.thy \
- GroupTheory/Exponent.thy GroupTheory/Exponent.ML GroupTheory/Group.thy\
- GroupTheory/Group.ML GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
+ GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
+ GroupTheory/Coset.thy GroupTheory/Coset.ML\
+ GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
+ GroupTheory/Group.thy GroupTheory/Group.ML\
+ GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
GroupTheory/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL GroupTheory