src/HOL/IsaMakefile
changeset 21423 6cdd0589aa73
parent 21317 ebd2704ed33b
child 21425 c11ab38b78a7
--- 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