New theory on divisibility;
Restructured presentation.
--- 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 \