20071021 
nipkow 
20071021 
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

file  diff  annotate 
20070927 
paulson 
20070927 
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions

file  diff  annotate 
20070724 
wenzelm 
20070724 
fixed proofs involving dvd;

file  diff  annotate 
20061108 
wenzelm 
20061108 
moved theories Parity, GCD, Binomial to Library;

file  diff  annotate 
20060830 
webertj 
20060830 
lin_arith_prover: splitting reverted because of performance loss

file  diff  annotate 
20060803 
ballarin 
20060803 
Restructured algebra library, added ideals and quotient rings.

file  diff  annotate 
20060802 
webertj 
20060802 
lin_arith_prover splits certain operators (e.g. min, max, abs)

file  diff  annotate 
20050707 
nipkow 
20050707 
linear arithmetic now takes "&" in assumptions apart.

file  diff  annotate 
20050701 
nipkow 
20050701 
prime is a predicate now.

file  diff  annotate 
20050617 
haftmann 
20050617 
migrated theory headers to new format

file  diff  annotate 
20040609 
paulson 
20040609 
moved some cardinality results into main HOL

file  diff  annotate 
20040506 
wenzelm 
20040506 
tuned document;

file  diff  annotate 
20030318 
paulson 
20030318 
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.
Deleted Ring, Module from GroupTheory
Minor UNITY changes

file  diff  annotate 