--- a/src/HOL/IsaMakefile Sun Nov 19 13:02:55 2006 +0100
+++ b/src/HOL/IsaMakefile Sun Nov 19 23:48:55 2006 +0100
@@ -385,37 +385,19 @@
HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
-$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
- Library/Primes.thy Library/FuncSet.thy \
- Algebra/AbelCoset.thy \
- Algebra/Bij.thy \
- Algebra/Coset.thy \
- Algebra/Exponent.thy \
- Algebra/FiniteProduct.thy \
- Algebra/Group.thy \
- Algebra/Ideal.thy \
- Algebra/Lattice.thy \
- Algebra/Module.thy \
- Algebra/Ring.thy \
- Algebra/Sylow.thy \
- Algebra/UnivPoly.thy \
- Algebra/IntRing.thy \
- Algebra/QuotRing.thy \
- Algebra/RingHom.thy \
- Algebra/abstract/Abstract.thy \
- Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
- Algebra/abstract/Field.thy \
- Algebra/abstract/Ideal2.ML Algebra/abstract/Ideal2.thy \
- Algebra/abstract/PID.thy \
- Algebra/abstract/Ring2.ML Algebra/abstract/Ring2.thy \
- Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
- Algebra/abstract/order.ML \
- Algebra/document/root.tex \
- Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
- Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
- Algebra/poly/Polynomial.thy \
- Algebra/poly/UnivPoly2.ML Algebra/poly/UnivPoly2.thy \
- Algebra/ringsimp.ML
+$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy \
+ Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy \
+ Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy \
+ Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \
+ Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \
+ Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \
+ Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy \
+ Algebra/abstract/Factor.thy Algebra/abstract/Field.thy \
+ Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy \
+ Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy \
+ Algebra/document/root.tex Algebra/poly/LongDiv.thy \
+ Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy \
+ Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
## HOL-Auth