# HG changeset patch
# User ballarin
# Date 1217340970 -7200
# Node ID bcf941cc33243fb52e568b7faa0e97e7a078a00c
# Parent  15b65db6675165dda5a57fc0f2dc7437367fcedb
New theory on divisibility;
Restructured presentation.

diff -r 15b65db66751 -r bcf941cc3324 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 29 16:14:56 2008 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 29 16:16:10 2008 +0200
@@ -504,9 +504,12 @@
 
 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	\
+$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML			\
+  Library/Binomial.thy Library/FuncSet.thy				\
+  Library/Multiset.thy Library/Permutation.thy Library/Primes.thy	\
+  Algebra/AbelCoset.thy Algebra/Bij.thy	Algebra/Congruence.thy		\
+  Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy	\
+  Algebra/FiniteProduct.thy Algebra/GLattice.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		\