1.1 --- a/src/HOL/IsaMakefile	Fri Nov 05 11:14:26 1999 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 05 12:45:37 1999 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  default: HOL
     1.6  images: HOL HOL-Real TLA
     1.7 -test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
     1.8 +test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
     1.9    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
    1.10    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
    1.11    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
    1.12 @@ -178,6 +178,28 @@
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL Lex
    1.14  
    1.15  
    1.16 +## HOL-Algebra
    1.17 +
    1.18 +HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
    1.19 +
    1.20 +$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
    1.21 +  Algebra/abstract/Abstract.thy \
    1.22 +  Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
    1.23 +  Algebra/abstract/Field.thy \
    1.24 +  Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \
    1.25 +  Algebra/abstract/NatSum.ML Algebra/abstract/NatSum.thy \
    1.26 +  Algebra/abstract/PID.thy \
    1.27 +  Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
    1.28 +  Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
    1.29 +  Algebra/poly/Degree.ML Algebra/poly/Degree.thy \
    1.30 +  Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
    1.31 +  Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
    1.32 +  Algebra/poly/PolyRing.ML Algebra/poly/PolyRing.thy \
    1.33 +  Algebra/poly/Polynomial.thy \
    1.34 +  Algebra/poly/ProtoPoly.ML Algebra/poly/ProtoPoly.thy \
    1.35 +  Algebra/poly/UnivPoly.ML Algebra/poly/UnivPoly.thy
    1.36 +	@$(ISATOOL) usedir $(OUT)/HOL Algebra
    1.37 +
    1.38  ## HOL-Auth
    1.39  
    1.40  HOL-Auth: HOL $(LOG)/HOL-Auth.gz